1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import analysis.calculus.fderiv
src         └──────────────────────┘
  8  
  9  /-!
 10  # Higher differentiability
 11  
 12  A function is `C^1` on a domain if it is differentiable there, and its derivative is continuous.
 13  By induction, it is `C^n` if it is `C^{n-1}` and its (n-1)-th derivative is `C^1` there or,
 14  equivalently, if it is `C^1` and its derivative is `C^{n-1}`.
 15  Finally, it is `C^∞` if it is `C^n` for all n.
 16  
 17  We formalize these notions by defining iteratively the n-th derivative of a function at the
 18  (n-1)-th derivative of the derivative. It is called `iterated_fderiv 𝕜 n f x` where `𝕜` is the
 19  field, `n` is the number of iterations, `f` is the function and `x` is the point. We also define a
 20  version `iterated_fderiv_within` relative to a domain, as well as predicates `times_cont_diff 𝕜 n f`
 21  and `times_cont_diff_on 𝕜 n f s` saying that the function is `C^n`, respectively in the whole space
 22  or on the set `s`.
 23  
 24  We prove basic properties of these notions.
 25  
 26  ## Implementation notes
 27  
 28  The n-th derivative of a function belongs to the space E →L[𝕜] (E →L[𝕜] (E ... F)...))),
 29  where there are n iterations of `E →L[𝕜]`. We define this space inductively, call it
 30  `iterated_continuous_linear_map 𝕜 n E F`, and denote it by `E [×n]→L[𝕜] F`. We can define
 31  it inductively either from the left (i.e., saying that the
 32  (n+1)-th space S_{n+1} is E →L[𝕜] S_n) or from the right (i.e., saying that
 33  the (n+1)-th space associated to F, denoted by S_{n+1} (F), is equal to S_n (E →L[𝕜] F)).
 34  For proofs, it turns out to be more convenient to use the latter approach (from the right),
 35  as it means to prove things at the (n+1)-th step we only need to understand well enough the
 36  derivative in E →L[𝕜] F (contrary to the approach from the left, where one would need to know
 37  enough on the n-th derivative to deduce things on the (n+1)-th derivative).
 38  In other words, one could define the (n+1)-th derivative either as the derivative of the n-th
 39  derivative, or as the n-th derivative of the derivative. We use the latter definition.
 40  
 41  A difficulty is related to universes: the first and second spaces in the sequence, for n=0
 42  and 1, are F and E →L[𝕜] F. If E has universe u and F has universe v, then the first one lives in
 43  v and the second one in max v u. Since they should live in the same universe (as all the other
 44  spaces in the construction), it means that at the 0-th step we should not use F, but ulift it to
 45  universe max v u. But we should also ulift its vector space structure and its normed space
 46  structure. This can certainly be done, but I decided it was not worth it for now. Therefore, the
 47  definition is only made when E and F live in the same universe.
 48  
 49  Regarding the definition of `C^n` functions, there are two equivalent definitions:
 50  * require by induction that the function is differentiable, and that its derivative is C^{n-1}
 51  * or require that, for all m ≤ n, the m-th derivative is continuous, and for all m < n the m-th
 52  derivative is differentiable.
 53  The first definition is more efficient for many proofs by induction. The second definition is more
 54  satisfactory as it gives concrete information about the n-th derivative (contrary to the first point
 55  of view), and moreover it also makes sense for n = ∞.
 56  
 57  Therefore, we give (and use) both definitions, named respectively `times_cont_diff_rec` and
 58  `times_cont_diff` (as well as relativized versions on a set). We show that they are equivalent.
 59  The first one is mainly auxiliary: in applications, one should always use `times_cont_diff`
 60  (but the proofs below use heavily the equivalence to show that `times_cont_diff` is well behaved).
 61  
 62  ## Tags
 63  
 64  derivative, differentiability, higher derivative, C^n
 65  
 66  -/
 67  
 68  noncomputable theory
 69  local attribute [instance, priority 10] classical.decidable_inhabited classical.prop_decidable
id                                           └───────────────────────────┘ └──────────────────────┘
src                                          └───────────────────────────┘ └──────────────────────┘
typ                                          └───────────────────────────┘ └──────────────────────┘
 70  
 71  universes u v w
 72  
 73  open set
 74  open_locale topological_space
 75  
 76  variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id                          └──────────────────────┘
src                         └──────────────────────┘
typ                         └──────────────────────┘
doc                         └──────────────────────┘
 77  {E : Type u} [normed_group E] [normed_space 𝕜 E]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
 78  {F : Type u} [normed_group F] [normed_space 𝕜 F]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
 79  {G : Type u} [normed_group G] [normed_space 𝕜 G]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
 80  {s s₁ u : set E} {f f₁ : E → F} {f' f₁' : E →L[𝕜] F} {f₂ : E → G}
id             └─┘                               └─┘ 
src            └─┘                               └─┘ 
typ            └─┘                               └─┘ 
doc                                              └─┘ 
 81  {f₂' : E →L[𝕜] G} {g : F → G} {x : E} {c : F}
id            └─┘ 
src           └─┘ 
typ           └─┘ 
doc           └─┘ 
 82  {L : filter E} {t : set F} {b : E × F → G} {sb : set (E × F)} {p : E × F}
id        └────┘         └─┘                         └─┘                
src       └────┘         └─┘                         └─┘                
typ       └────┘         └─┘                         └─┘                
 83  {n : ℕ}
id        
src       
typ       
 84  
 85  include 𝕜
 86  
 87  /--
 88  The space `iterated_continuous_linear_map 𝕜 n E F` is the space E →L[𝕜] (E →L[𝕜] (E ... F)...))),
 89  defined inductively over `n`. This is the space to which the `n`-th derivative of a function
 90  naturally belongs. It is only defined when `E` and `F` live in the same universe.
 91  -/
 92  def iterated_continuous_linear_map (𝕜 : Type w) [nondiscrete_normed_field 𝕜] :
id                                                    └──────────────────────┘ 
src                                                   └──────────────────────┘
typ                                                   └──────────────────────┘ 
doc                                                   └──────────────────────┘
 93    Π (n : ℕ) (E : Type u) [gE : normed_group E] [@normed_space 𝕜 E _ gE]
id                  └──┘          └──────────┘     └──────────┘     └┘
src                                └──────────┘      └──────────┘
typ                 └──┘          └──────────┘     └──────────┘     └┘
doc                                 └──────────┘      └──────────┘
 94      (F : Type u) [gF : normed_group F] [@normed_space 𝕜 F _ gF], Type u
id            └──┘          └──────────┘     └──────────┘     └┘
src                         └──────────┘      └──────────┘
typ           └──┘          └──────────┘     └──────────┘     └┘
doc                         └──────────┘      └──────────┘
 95  | 0     E _ _ F _ _ := F
id                 
typ                
 96  | (n+1) E _ _ F _ _ := by { resetI, exact iterated_continuous_linear_map n E (E →L[𝕜] F) }
id                                            └────────────────────────────┘      └─┘ 
src                             └────┘  └────┘                                  └─┘  └┘
typ                             └────┘  └────┘└────────────────────────────┘  └─┘└┘
doc                              └────┘  └────┘                                  └─┘  └┘
txt                              └────┘  └────┘                                        └┘
par                              └────┘  └────┘                                        └┘
pid                                                                                   
st                            └──────────────────────────────────────────────────────────────┘└┘
 97  
 98  notation E `[×`:25 n `]→L[`:25 𝕜 `] ` F := iterated_continuous_linear_map 𝕜 n E F
id                                              └────────────────────────────┘
src                                             └────────────────────────────┘
typ                                             └────────────────────────────┘
doc                                             └────────────────────────────┘
 99  
100  /--
101  Define by induction a normed group structure on the space of iterated continuous linear
102  maps. To avoid `resetI` in the statement, use the @ version with all parameters. As the equation
103  compiler chokes on this one, we use the `nat.rec_on` version.
104  -/
105  def iterated_continuous_linear_map.normed_group_rec (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id                                                                          └──────────────────────┘ 
src                                                                         └──────────────────────┘
typ                                                                         └──────────────────────┘ 
doc                                                                         └──────────────────────┘
106    (n : ℕ) (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E] :
id                               └──────────┘         └──────────┘  
src                              └──────────┘          └──────────┘
typ                              └──────────┘         └──────────┘  
doc                               └──────────┘          └──────────┘
107    ∀(F : Type u) [nF : normed_group F] [sF : @normed_space 𝕜 F _ nF],
id           └──┘          └──────────┘          └──────────┘     └┘
src                        └──────────┘           └──────────┘
typ          └──┘          └──────────┘          └──────────┘     └┘
doc                        └──────────┘           └──────────┘
108    normed_group (@iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F nF sF) :=
id     └──────────┘   └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
src    └──────────┘   └────────────────────────────┘
typ    └──────────┘   └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
doc    └──────────┘   └────────────────────────────┘
109  nat.rec_on n (λF nF sF, nF) (λn aux_n F nF sF, by { resetI, apply aux_n })
id   └────────┘     └┘ └┘  └┘     └───┘  └┘ └┘
src  └────────┘                                          └────┘  └────┘     
typ  └────────┘     └┘ └┘  └┘     └───┘  └┘ └┘       └────┘  └────┘     
doc                                                      └────┘  └────┘     
txt                                                      └────┘  └────┘     
par                                                      └────┘  └────┘     
pid                                                                        
st                                                    └─────────────────────┘└┘
110  
111  /--
112  Define by induction a normed space structure on the space of iterated continuous linear
113  maps. To avoid `resetI` in the statement, use the @ version with all parameters. As the equation
114  compiler chokes on this one, we use the `nat.rec_on` version.
115  -/
116  def iterated_continuous_linear_map.normed_space_rec (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id                                                                          └──────────────────────┘ 
src                                                                         └──────────────────────┘
typ                                                                         └──────────────────────┘ 
doc                                                                         └──────────────────────┘
117    (n : ℕ) (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E] :
id                               └──────────┘         └──────────┘  
src                              └──────────┘          └──────────┘
typ                              └──────────┘         └──────────┘  
doc                               └──────────┘          └──────────┘
118    ∀(F : Type u) [nF : normed_group F] [sF : @normed_space 𝕜 F _ nF],
id           └──┘          └──────────┘          └──────────┘     └┘
src                        └──────────┘           └──────────┘
typ          └──┘          └──────────┘          └──────────┘     └┘
doc                        └──────────┘           └──────────┘
119    @normed_space 𝕜 (@iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F nF sF)
id      └──────────┘    └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
src     └──────────┘     └────────────────────────────┘
typ     └──────────┘    └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
doc     └──────────┘     └────────────────────────────┘
120    _ (@iterated_continuous_linear_map.normed_group_rec 𝕜 h𝕜 n E gE sE F nF sF) :=
id         └─────────────────────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
src        └─────────────────────────────────────────────┘
typ        └─────────────────────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
doc        └─────────────────────────────────────────────┘
121  nat.rec_on n (λF nF sF, sF) (λn aux_n F nF sF, by { resetI, apply aux_n })
id   └────────┘     └┘ └┘  └┘     └───┘  └┘ └┘
src  └────────┘                                          └────┘  └────┘     
typ  └────────┘     └┘ └┘  └┘     └───┘  └┘ └┘       └────┘  └────┘     
doc                                                      └────┘  └────┘     
txt                                                      └────┘  └────┘     
par                                                      └────┘  └────┘     
pid                                                                        
st                                                    └─────────────────────┘└┘
122  
123  /--
124  Explicit normed group structure on the space of iterated continuous linear maps.
125  -/
126  instance iterated_continuous_linear_map.normed_group (n : ℕ)
id                                                             
src                                                            
typ                                                            
127    (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id                        └──────────────────────┘ 
src                       └──────────────────────┘
typ                       └──────────────────────┘ 
doc                       └──────────────────────┘
128    (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E]
id                        └──────────┘         └──────────┘  
src                       └──────────┘          └──────────┘
typ                       └──────────┘         └──────────┘  
doc                       └──────────┘          └──────────┘
129    (F : Type u) [gF : normed_group F] [sF : normed_space 𝕜 F] :
id                        └──────────┘         └──────────┘  
src                       └──────────┘          └──────────┘
typ                       └──────────┘         └──────────┘  
doc                       └──────────┘          └──────────┘
130    normed_group (E [×n]→L[𝕜] F) :=
id     └──────────┘   └┘└──┘ 
src    └──────────┘    └┘ └──┘ 
typ    └──────────┘   └┘└──┘ 
doc    └──────────┘    └┘ └──┘ 
131  iterated_continuous_linear_map.normed_group_rec 𝕜 n E F
id   └─────────────────────────────────────────────┘    
src  └─────────────────────────────────────────────┘
typ  └─────────────────────────────────────────────┘    
doc  └─────────────────────────────────────────────┘
132  
133  instance : inhabited (E [×n]→L[𝕜] F) := ⟨0⟩
id              └───────┘   └┘└──┘ 
src             └───────┘    └┘ └──┘ 
typ             └───────┘   └┘└──┘ 
doc                          └┘ └──┘ 
134  
135  /--
136  Explicit normed space structure on the space of iterated continuous linear maps.
137  -/
138  instance iterated_continuous_linear_map.normed_space (n : ℕ)
id                                                             
src                                                            
typ                                                            
139    (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id                        └──────────────────────┘ 
src                       └──────────────────────┘
typ                       └──────────────────────┘ 
doc                       └──────────────────────┘
140    (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E]
id                        └──────────┘         └──────────┘  
src                       └──────────┘          └──────────┘
typ                       └──────────┘         └──────────┘  
doc                       └──────────┘          └──────────┘
141    (F : Type u) [gF : normed_group F] [sF : normed_space 𝕜 F] :
id                        └──────────┘         └──────────┘  
src                       └──────────┘          └──────────┘
typ                       └──────────┘         └──────────┘  
doc                       └──────────┘          └──────────┘
142    normed_space 𝕜 (E [×n]→L[𝕜] F) :=
id     └──────────┘    └┘└──┘ 
src    └──────────┘      └┘ └──┘ 
typ    └──────────┘    └┘└──┘ 
doc    └──────────┘      └┘ └──┘ 
143  iterated_continuous_linear_map.normed_space_rec 𝕜 n E F
id   └─────────────────────────────────────────────┘    
src  └─────────────────────────────────────────────┘
typ  └─────────────────────────────────────────────┘    
doc  └─────────────────────────────────────────────┘
144  
145  /--
146  The n-th derivative of a function, defined inductively by saying that the (n+1)-th
147  derivative of f is the n-th derivative of the derivative of f.
148  -/
149  def iterated_fderiv (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜] (n : ℕ)
id                                          └──────────────────────┘        
src                                         └──────────────────────┘         
typ                                         └──────────────────────┘        
doc                                         └──────────────────────┘
150    {E : Type u} [gE : normed_group E] [sE : normed_space 𝕜 E] :
id                        └──────────┘         └──────────┘  
src                       └──────────┘          └──────────┘
typ                       └──────────┘         └──────────┘  
doc                       └──────────┘          └──────────┘
151    ∀{F : Type u} [gF : normed_group F] [sF : @normed_space 𝕜 F _ gF] (f : E → F),
id           └──┘          └──────────┘          └──────────┘     └┘         
src                        └──────────┘           └──────────┘
typ          └──┘          └──────────┘          └──────────┘     └┘         
doc                        └──────────┘           └──────────┘
152    E → @iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F gF sF :=
id         └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
src         └────────────────────────────┘
typ        └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
doc         └────────────────────────────┘
153  nat.rec_on n (λF gF sF f, f) (λn rec F gF sF f, by { resetI, exact rec (fderiv 𝕜 f) })
id   └────────┘     └┘ └┘        └─┘  └┘ └┘                      └─┘  └────┘  
src  └────────┘                                           └────┘  └────┘    └────┘  └┘
typ  └────────┘     └┘ └┘        └─┘  └┘ └┘        └────┘  └────┘└─┘ └────┘└┘
doc                                                       └────┘  └────┘    └────┘  └┘
txt                                                       └────┘  └────┘            └┘
par                                                       └────┘  └────┘            └┘
pid                                                                                
st                                                     └────────────────────────────────┘└┘
154  
155  @[simp] lemma iterated_fderiv_zero :
doc    └──┘
156    iterated_fderiv 𝕜 0 f = f := rfl
id     └─────────────┘          └─┘
src    └─────────────┘             └─┘
typ    └─────────────┘          └─┘
doc    └─────────────┘
157  
158  @[simp] lemma iterated_fderiv_succ :
doc    └──┘
159    iterated_fderiv 𝕜 (n+1) f = (iterated_fderiv 𝕜 n (λx, fderiv 𝕜 f x) : _) := rfl
id     └─────────────┘         └─────────────┘       └────┘             └─┘
src    └─────────────┘            └─────────────┘          └────┘                └─┘
typ    └─────────────┘         └─────────────┘       └────┘             └─┘
doc    └─────────────┘              └─────────────┘          └────┘
160  
161  /--
162  The n-th derivative of a function along a set, defined inductively by saying that the (n+1)-th
163  derivative of f is the n-th derivative of the derivative of f.
164  -/
165  def iterated_fderiv_within (𝕜 : Type w) [h𝕜 :nondiscrete_normed_field 𝕜] (n : ℕ)
id                                                └──────────────────────┘        
src                                               └──────────────────────┘         
typ                                               └──────────────────────┘        
doc                                               └──────────────────────┘
166    {E : Type u} [gE : normed_group E] [sE : normed_space 𝕜 E] :
id                        └──────────┘         └──────────┘  
src                       └──────────┘          └──────────┘
typ                       └──────────┘         └──────────┘  
doc                       └──────────┘          └──────────┘
167    ∀{F : Type u} [gF : normed_group F] [sF : @normed_space 𝕜 F _ gF] (f : E → F) (s : set E),
id           └──┘          └──────────┘          └──────────┘     └┘                └─┘ 
src                        └──────────┘           └──────────┘                            └─┘
typ          └──┘          └──────────┘          └──────────┘     └┘                └─┘ 
doc                        └──────────┘           └──────────┘
168    E → @iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F gF sF :=
id         └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
src         └────────────────────────────┘
typ        └────────────────────────────┘  └┘   └┘ └┘  └┘ └┘
doc         └────────────────────────────┘
169  nat.rec_on n (λF gF sF f s, f) (λn rec F gF sF f s, by { resetI, exact rec (fderiv_within 𝕜 f s) s})
id   └────────┘     └┘ └┘         └─┘  └┘ └┘                       └─┘  └───────────┘      
src  └────────┘                                               └────┘  └────┘    └───────────┘   └┘
typ  └────────┘     └┘ └┘         └─┘  └┘ └┘         └────┘  └────┘└─┘ └───────────┘ └┘
doc                                                           └────┘  └────┘    └───────────┘   └┘
txt                                                           └────┘  └────┘                    └┘
par                                                           └────┘  └────┘                    └┘
pid                                                                                            └┘
st                                                         └──────────────────────────────────────────┘└┘
170  
171  @[simp] lemma iterated_fderiv_within_zero :
doc    └──┘
172    iterated_fderiv_within 𝕜 0 f s = f := rfl
id     └────────────────────┘           └─┘
src    └────────────────────┘               └─┘
typ    └────────────────────┘           └─┘
doc    └────────────────────┘
173  
174  @[simp] lemma iterated_fderiv_within_succ :
doc    └──┘
175    iterated_fderiv_within 𝕜 (n+1) f s
id     └────────────────────┘       
src    └────────────────────┘     
typ    └────────────────────┘       
doc    └────────────────────┘
176    = (iterated_fderiv_within 𝕜 n (λx, fderiv_within 𝕜 f s x) s : _) := rfl
id       └────────────────────┘       └───────────┘               └─┘
src      └────────────────────┘          └───────────┘                    └─┘
typ      └────────────────────┘       └───────────┘               └─┘
doc       └────────────────────┘          └───────────┘
177  
178  theorem iterated_fderiv_within_univ {n : ℕ} :
id                                            
src                                           
typ                                           
179    iterated_fderiv_within 𝕜 n f univ = iterated_fderiv 𝕜 n f :=
id     └────────────────────┘    └──┘  └─────────────┘   
src    └────────────────────┘       └──┘  └─────────────┘
typ    └────────────────────┘    └──┘  └─────────────┘   
doc    └────────────────────┘              └─────────────┘
180  begin
st   └─────
181    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
182    induction n with n IH generalizing F,
id               
src    └────────┘ └───────────────────────┘
typ    └────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────┘
txt    └────────┘ └───────────────────────┘
par    └────────┘ └───────────────────────┘
pid              └───────┘└─────────────┘
st   ─────────────────────────────────────┘└─
183    { refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
184    { simp [IH] }
src      └────┘  └┘
typ      └────┘└┘└┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid            
st   ─────────────┘└─
185  end
st   ──┘
186  
187  /--
188  If two functions coincide on a set `s` of unique differentiability, then their iterated
189  differentials within this set coincide.
190  -/
191  lemma iterated_fderiv_within_congr (hs : unique_diff_on 𝕜 s)
id                                            └────────────┘  
src                                           └────────────┘
typ                                           └────────────┘  
doc                                           └────────────┘
192    (hL : ∀y∈s, f₁ y = f y) (hx : x ∈ s) :
id               └┘              
src                                  
typ              └┘              
193    iterated_fderiv_within 𝕜 n f₁ s x = iterated_fderiv_within 𝕜 n f s x :=
id     └────────────────────┘   └┘    └────────────────────┘     
src    └────────────────────┘             └────────────────────┘
typ    └────────────────────┘   └┘    └────────────────────┘     
doc    └────────────────────┘              └────────────────────┘
194  begin
st   └─────
195    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
196    induction n with n IH generalizing F f x,
id               
src    └────────┘ └───────────────────────────┘
typ    └────────┘└───────────────────────────┘
doc    └────────┘ └───────────────────────────┘
txt    └────────┘ └───────────────────────────┘
par    └────────┘ └───────────────────────────┘
pid              └───────┘└─────────────────┘
st   ─────────────────────────────────────────┘└─
197    { simp [hL x hx] },
id             └┘  └┘
src      └────┘     └┘
typ      └────┘└┘└┘└┘
doc      └────┘     └┘
txt      └────┘     └┘
par      └────┘     └┘
pid               
st   ───┘└─────────────┘└┘
198    { simp only [iterated_fderiv_within_succ],
id                  └─────────────────────────┘
src      └─────────┘└─────────────────────────┘
typ      └─────────┘└─────────────────────────┘
doc      └─────────┘                           
txt      └─────────┘                           
par      └─────────┘                           
pid          └──┘└┘                           
st   ──────────────────────────────────────────┘└─
199      refine IH (λy hy, _) hx,
id              └┘            └┘
src      └─────┘    └───────┘
typ      └─────┘└┘  └───────┘└┘
doc      └─────┘    └───────┘
txt      └─────┘    └───────┘
par      └─────┘    └───────┘
pid                └───────┘
st   ──────────────────────────┘└─
200      apply fderiv_within_congr (hs y hy) hL (hL y hy) }
id             └─────────────────┘  └┘           └┘  └┘
src      └────┘└─────────────────┘      └┘        └┘
typ      └────┘└─────────────────┘ └┘   └┘   └┘└┘└┘
doc      └────┘                         └┘        └┘
txt      └────┘                         └┘        └┘
par      └────┘                         └┘        └┘
pid                                    └┘        
st   ────────────────────────────────────────────────────┘└─
201  end
st   ──┘
202  
203  /--
204  The iterated differential within a set `s` at a point `x` is not modified if one intersects
205  `s` with an open set containing `x`.
206  -/
207  lemma iterated_fderiv_within_inter_open (xu : x ∈ u) (hu : is_open u) (xs : x ∈ s)
id                                                           └─────┘           
src                                                            └─────┘            
typ                                                          └─────┘           
doc                                                             └─────┘
208    (hs : unique_diff_on 𝕜 (s ∩ u)) :
id           └────────────┘     
src          └────────────┘      
typ          └────────────┘     
doc          └────────────┘
209    iterated_fderiv_within 𝕜 n f (s ∩ u) x = iterated_fderiv_within 𝕜 n f s x :=
id     └────────────────────┘           └────────────────────┘     
src    └────────────────────┘                 └────────────────────┘
typ    └────────────────────┘           └────────────────────┘     
doc    └────────────────────┘                   └────────────────────┘
210  begin
st   └─────
211    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
212    induction n with n IH generalizing F f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
213    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
214    { simp,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
215      rw ← IH,
src      └───┘
typ      └───┘└┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ──────────┘└─
216      apply iterated_fderiv_within_congr hs (λy hy, _) ⟨xs, xu⟩,
id             └──────────────────────────┘ └┘             └┘  └┘
src      └────┘└──────────────────────────┘    └───────┘   └┘  
typ      └────┘└──────────────────────────┘└┘  └───────┘ └┘└┘└┘
doc      └────┘└──────────────────────────┘    └───────┘   └┘  
txt      └────┘                                └───────┘   └┘  
par      └────┘                                └───────┘   └┘  
pid                                           └───────┘   └┘  
st   ────────────────────────────────────────────────────────────┘└─
217      apply fderiv_within_inter (mem_nhds_sets hu hy.2),
id             └─────────────────┘  └───────────┘ └┘ └┘
src      └────┘└─────────────────┘ └───────────┘    └─┘
typ      └────┘└─────────────────┘ └───────────┘└┘└┘└─┘
doc      └────┘                                     └─┘
txt      └────┘                                     └─┘
par      └────┘                                     └─┘
pid                                                └─┘
st   ────────────────────────────────────────────────────┘└─
218      have := hs y hy,
id               └┘  └┘
src      └──────┘   
typ      └──────┘└┘└┘
doc      └──────┘   
txt      └──────┘   
par      └──────┘   
pid      └───┘└─┘   
st   ──────────────────┘└─
219      rwa unique_diff_within_at_inter (mem_nhds_sets hu hy.2) at this }
id           └─────────────────────────┘  └───────────┘ └┘ └┘
src      └──┘└─────────────────────────┘ └───────────┘    └──────────┘
typ      └──┘└─────────────────────────┘ └───────────┘└┘└┘└──────────┘
doc      └──┘                                             └──────────┘
txt      └──┘                                             └──────────┘
par      └──┘                                             └──────────┘
pid                                                      └─┘└──────┘
st   ───────────────────────────────────────────────────────────────────┘└─
220  end
st   ──┘
221  
222  /--
223  The iterated differential within a set `s` at a point `x` is not modified if one intersects
224  `s` with a neighborhood of `x`.
225  -/
226  lemma iterated_fderiv_within_inter (hu : u ∈ 𝓝 x) (xs : x ∈ s)
id                                                         
src                                                          
typ                                                        
doc                                               
227    (hs : unique_diff_on 𝕜 s) :
id           └────────────┘  
src          └────────────┘
typ          └────────────┘  
doc          └────────────┘
228    iterated_fderiv_within 𝕜 n f (s ∩ u) x = iterated_fderiv_within 𝕜 n f s x :=
id     └────────────────────┘           └────────────────────┘     
src    └────────────────────┘                 └────────────────────┘
typ    └────────────────────┘           └────────────────────┘     
doc    └────────────────────┘                   └────────────────────┘
229  begin
st   └─────
230    rcases mem_nhds_sets_iff.1 hu with ⟨v, vu, v_open, xv⟩,
id            └───────────────┘   └┘
src    └─────┘└───────────────┘└─┘  └───────────────────────┘
typ    └─────┘└───────────────┘└─┘└┘└───────────────────────┘
doc    └─────┘                 └─┘  └───────────────────────┘
txt    └─────┘                 └─┘  └───────────────────────┘
par    └─────┘                 └─┘  └───────────────────────┘
pid                           └─┘  └───────────────────────┘
st   ───────────────────────────────────────────────────────┘└─
231    have A : (s ∩ u) ∩ v = s ∩ v,
id                            
src    └───────┘   └┘    
typ    └───────┘  └┘   
doc    └───────┘    └┘     
txt    └───────┘    └┘     
par    └───────┘    └┘     
pid    └────┘└─┘    └┘     
st   ─────────────────────────────┘└─
232    { apply subset.antisymm (inter_subset_inter (inter_subset_left _ _) (subset.refl _)),
id             └─────────────┘  └────────────────┘  └───────────────┘       └─────────┘
src      └────┘└─────────────┘ └────────────────┘ └───────────────┘└────┘ └─────────┘└──┘
typ      └────┘└─────────────┘ └────────────────┘ └───────────────┘└────┘ └─────────┘└──┘
doc      └────┘                                                    └────┘            └──┘
txt      └────┘                                                    └────┘            └──┘
par      └────┘                                                    └────┘            └──┘
pid                                                               └────┘            └──┘
st   ───┘└────────────────────────────────────────────────────────────────────────────────┘└─
233      exact λ y ⟨ys, yv⟩, ⟨⟨ys, vu yv⟩, yv⟩ },
id                  └┘  └┘         └┘
src      └────┘ └──┘  └┘  └─┘    └┘    └─┘  └┘
typ      └────┘ └──┘└┘└┘└┘└─┘    └┘└┘  └─┘  └┘
doc      └────┘ └──┘  └┘  └─┘    └┘    └─┘  └┘
txt      └────┘ └──┘  └┘  └─┘    └┘    └─┘  └┘
par      └────┘ └──┘  └┘  └─┘    └┘    └─┘  └┘
pid            └──┘  └┘  └─┘    └┘    └─┘  
st   ─────────────────────────────────────────┘└┘
234    have : iterated_fderiv_within 𝕜 n f (s ∩ v) x = iterated_fderiv_within 𝕜 n f s x :=
id                                                    └────────────────────┘     
src    └─────┘                             └┘  └────────────────────┘     └───
typ    └─────┘                            └┘  └────────────────────┘└───
doc    └─────┘                             └┘  └────────────────────┘     └───
txt    └─────┘                             └┘                             └───
par    └─────┘                             └┘                             └───
pid    └───┘└┘                             └┘                             └───
st   ──────────────────────────────────────────────────────────────────────────────────────
235      iterated_fderiv_within_inter_open xv v_open xs (hs.inter v_open),
id       └───────────────────────────────┘ └┘        └┘  └──────┘ └────┘
src  ───┘└───────────────────────────────┘           └──────┘      
typ  ───┘└───────────────────────────────┘└┘      └┘ └──────┘└────┘
doc  ───┘└───────────────────────────────┘                         
txt  ───┘                                                          
par  ───┘                                                          
pid  ───┘                                                          
st   ───────────────────────────────────────────────────────────────────┘└─
236    rw ← this,
id          └──┘
src    └───┘
typ    └───┘└──┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ──────────┘└─
237    have : iterated_fderiv_within 𝕜 n f ((s ∩ u) ∩ v) x = iterated_fderiv_within 𝕜 n f (s ∩ u) x,
id                                                          └────────────────────┘          
src    └─────┘                              └┘  └┘  └────────────────────┘       └┘
typ    └─────┘                              └┘ └┘  └────────────────────┘  └┘
doc    └─────┘                              └┘  └┘  └────────────────────┘       └┘
txt    └─────┘                              └┘  └┘                               └┘
par    └─────┘                              └┘  └┘                               └┘
pid    └───┘└┘                              └┘  └┘                               └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘└─
238    { refine iterated_fderiv_within_inter_open xv v_open ⟨xs, mem_of_nhds hu⟩ _,
id              └───────────────────────────────┘ └┘ └────┘  └┘  └─────────┘ └┘
src      └─────┘└───────────────────────────────┘           └┘└─────────┘  └─┘
typ      └─────┘└───────────────────────────────┘└┘└────┘ └┘└┘└─────────┘└┘└─┘
doc      └─────┘└───────────────────────────────┘           └┘             └─┘
txt      └─────┘                                            └┘             └─┘
par      └─────┘                                            └┘             └─┘
pid                                                        └┘             └─┘
st   ───┘└───────────────────────────────────────────────────────────────────────┘└─
239      rw A,
id          
src      └─┘
typ      └─┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────┘└─
240      exact hs.inter v_open },
id             └──────┘ └────┘
src      └────┘└──────┘      
typ      └────┘└──────┘└────┘
doc      └────┘              
txt      └────┘              
par      └────┘              
pid                         
st   ─────────────────────────┘└┘
241    rw A at this,
id        
src    └─┘ └──────┘
typ    └─┘└──────┘
doc    └─┘ └──────┘
txt    └─┘ └──────┘
par    └─┘ └──────┘
pid       └──────┘
st   ─────────────┘└─
242    rw ← this
id          └──┘
src    └───┘    
typ    └───┘└──┘
doc    └───┘    
txt    └───┘    
par    └───┘    
pid      └─┘    
st   ───────────┘
243  end
st   └─┘
244  
245  /--
246  Auxiliary definition defining `C^n` functions by induction over `n`.
247  In applications, use `times_cont_diff` instead.
248  -/
249  def times_cont_diff_rec (𝕜 : Type w) [nondiscrete_normed_field 𝕜] :
id                                         └──────────────────────┘ 
src                                        └──────────────────────┘
typ                                        └──────────────────────┘ 
doc                                        └──────────────────────┘
250    Π (n : ℕ) {E : Type u} [gE : normed_group E] [@normed_space 𝕜 E _ gE]
id                  └──┘          └──────────┘     └──────────┘     └┘
src                                └──────────┘      └──────────┘
typ                 └──┘          └──────────┘     └──────────┘     └┘
doc                                 └──────────┘      └──────────┘
251      {F : Type u} [gF : normed_group F] [@normed_space 𝕜 F _ gF] (f : E → F), Prop
id            └──┘          └──────────┘     └──────────┘     └┘         
src                         └──────────┘      └──────────┘
typ           └──┘          └──────────┘     └──────────┘     └┘         
doc                         └──────────┘      └──────────┘
252  | 0     E _ _ F _ _ f := by { resetI, exact continuous f }
id                                               └────────┘ 
src                                └────┘  └────┘└────────┘ 
typ                                └────┘  └────┘└────────┘
doc                                └────┘  └────┘└────────┘ 
txt                                └────┘  └────┘           
par                                └────┘  └────┘           
pid                                                        
st                              └────────────────────────────┘└┘
253  | (n+1) E _ _ F _ _ f := by { resetI, exact differentiable 𝕜 f ∧ times_cont_diff_rec n (fderiv 𝕜 f) }
id                                              └────────────┘       └─────────────────┘   └────┘  
src                               └────┘  └────┘└────────────┘                        └────┘  └┘
typ                               └────┘  └────┘└────────────┘   └─────────────────┘ └────┘└┘
doc                                └────┘  └────┘└────────────┘                        └────┘  └┘
txt                                └────┘  └────┘                                              └┘
par                                └────┘  └────┘                                              └┘
pid                                                                                           
st                              └───────────────────────────────────────────────────────────────────────┘└┘
254  
255  @[simp] lemma times_cont_diff_rec_zero :
doc    └──┘
256    times_cont_diff_rec 𝕜 0 f ↔ continuous f :=
id     └─────────────────┘      └────────┘ 
src    └─────────────────┘        └────────┘
typ    └─────────────────┘      └────────┘ 
doc    └─────────────────┘         └────────┘
257  by refl
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
258  
src  
typ  
doc  
txt  
par  
pid  
st   
259  @[simp] lemma times_cont_diff_rec_succ :
doc    └──┘
260    times_cont_diff_rec 𝕜 n.succ f ↔
id     └─────────────────┘  └───┘  
src    └─────────────────┘    └───┘   
typ    └─────────────────┘  └───┘  
doc    └─────────────────┘
261    differentiable 𝕜 f ∧ times_cont_diff_rec 𝕜 n (λx, fderiv 𝕜 f x) :=
id     └────────────┘    └─────────────────┘       └────┘   
src    └────────────┘      └─────────────────┘          └────┘
typ    └────────────┘    └─────────────────┘       └────┘   
doc    └────────────┘       └─────────────────┘          └────┘
262  by refl
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
263  
src  
typ  
doc  
txt  
par  
pid  
st   
264  lemma times_cont_diff_rec.of_succ (h : times_cont_diff_rec 𝕜 n.succ f) :
id                                          └─────────────────┘  └───┘ 
src                                         └─────────────────┘    └───┘
typ                                         └─────────────────┘  └───┘ 
doc                                         └─────────────────┘
265    times_cont_diff_rec 𝕜 n f :=
id     └─────────────────┘   
src    └─────────────────┘
typ    └─────────────────┘   
doc    └─────────────────┘
266  begin
st   └─────
267    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
268    induction n with n IH generalizing F,
id               
src    └────────┘ └───────────────────────┘
typ    └────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────┘
txt    └────────┘ └───────────────────────┘
par    └────────┘ └───────────────────────┘
pid              └───────┘└─────────────┘
st   ─────────────────────────────────────┘└─
269    { exact h.1.continuous },
id             
src      └────┘ └────────────┘
typ      └────┘└────────────┘
doc      └────┘ └────────────┘
txt      └────┘ └────────────┘
par      └────┘ └────────────┘
pid            └──────────┘└┘
st   ───┘└───────────────────┘└┘
270    { rw times_cont_diff_rec_succ at h ⊢,
id          └──────────────────────┘
src      └─┘└──────────────────────┘└─────┘
typ      └─┘└──────────────────────┘└─────┘
doc      └─┘                        └─────┘
txt      └─┘                        └─────┘
par      └─┘                        └─────┘
pid                                └─────┘
st   ─────────────────────────────────────┘└─
271      exact ⟨h.1, IH h.2⟩ }
id                   └┘ 
src      └────┘  └──┘   └──┘
typ      └────┘  └──┘└┘└──┘
doc      └────┘  └──┘   └──┘
txt      └────┘  └──┘   └──┘
par      └────┘  └──┘   └──┘
pid             └──┘   └─┘
st   ───────────────────────┘└─
272  end
st   ──┘
273  
274  lemma times_cont_diff_rec.continuous (h : times_cont_diff_rec 𝕜 n f) :
id                                             └─────────────────┘   
src                                            └─────────────────┘
typ                                            └─────────────────┘   
doc                                            └─────────────────┘
275    continuous (iterated_fderiv 𝕜 n f) :=
id     └────────┘  └─────────────┘   
src    └────────┘  └─────────────┘
typ    └────────┘  └─────────────┘   
doc    └────────┘  └─────────────┘
276  begin
st   └─────
277    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
278    induction n with n IH generalizing F f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
279    { exact h },
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───┘└──────┘└┘
280    { rw iterated_fderiv_succ,
id          └──────────────────┘
src      └─┘└──────────────────┘
typ      └─┘└──────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────────┘└─
281      exact IH (times_cont_diff_rec_succ.1 h).2 }
id             └┘  └──────────────────────┘   
src      └────┘   └──────────────────────┘└─┘ └──┘
typ      └────┘└┘ └──────────────────────┘└─┘└──┘
doc      └────┘                           └─┘ └──┘
txt      └────┘                           └─┘ └──┘
par      └────┘                           └─┘ └──┘
pid                                      └─┘ └─┘
st   ─────────────────────────────────────────────┘└─
282  end
st   ──┘
283  
284  lemma times_cont_diff_rec.differentiable (h : times_cont_diff_rec 𝕜 (n+1) f) :
id                                                 └─────────────────┘      
src                                                └─────────────────┘     
typ                                                └─────────────────┘      
doc                                                └─────────────────┘
285    differentiable 𝕜 (iterated_fderiv 𝕜 n f) :=
id     └────────────┘   └─────────────┘   
src    └────────────┘    └─────────────┘
typ    └────────────┘   └─────────────┘   
doc    └────────────┘    └─────────────┘
286  begin
st   └─────
287    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
288    induction n with n IH generalizing F f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
289    { exact h.1 },
id             
src      └────┘ └─┘
typ      └────┘└─┘
doc      └────┘ └─┘
txt      └────┘ └─┘
par      └────┘ └─┘
pid            └─┘
st   ───┘└────────┘└┘
290    { rw iterated_fderiv_succ,
id          └──────────────────┘
src      └─┘└──────────────────┘
typ      └─┘└──────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────────┘└─
291      apply IH h.2 }
id             └┘ 
src      └────┘   └─┘
typ      └────┘└┘└─┘
doc      └────┘   └─┘
txt      └────┘   └─┘
par      └────┘   └─┘
pid              └─┘
st   ────────────────┘└─
292  end
st   ──┘
293  
294  /--
295  Auxiliary definition defining `C^n` functions on a set by induction over `n`.
296  In applications, use `times_cont_diff_on` instead.
297  -/
298  def times_cont_diff_on_rec (𝕜 : Type w) [nondiscrete_normed_field 𝕜] :
id                                            └──────────────────────┘ 
src                                           └──────────────────────┘
typ                                           └──────────────────────┘ 
doc                                           └──────────────────────┘
299    Π (n : ℕ) {E : Type u} [gE : normed_group E] [@normed_space 𝕜 E _ gE]
id                  └──┘          └──────────┘     └──────────┘     └┘
src                                └──────────┘      └──────────┘
typ                 └──┘          └──────────┘     └──────────┘     └┘
doc                                 └──────────┘      └──────────┘
300      {F : Type u} [gF : normed_group F] [@normed_space 𝕜 F _ gF] (f : E → F) (s : set E), Prop
id            └──┘          └──────────┘     └──────────┘     └┘                └─┘ 
src                         └──────────┘      └──────────┘                            └─┘
typ           └──┘          └──────────┘     └──────────┘     └┘                └─┘ 
doc                         └──────────┘      └──────────┘
301  | 0     E _ _ F _ _ f s := by { resetI, exact continuous_on f s }
id                                                 └───────────┘  
src                                  └────┘  └────┘└───────────┘  
typ                                  └────┘  └────┘└───────────┘
doc                                  └────┘  └────┘└───────────┘  
txt                                  └────┘  └────┘               
par                                  └────┘  └────┘               
pid                                                              
st                                └─────────────────────────────────┘└┘
302  | (n+1) E _ _ F _ _ f s := by { resetI,
id       
src                                 └────┘
typ                                 └────┘
doc                                  └────┘
txt                                  └────┘
par                                  └────┘
st                                └──────────
303                    exact differentiable_on 𝕜 f s ∧ times_cont_diff_on_rec n (fderiv_within 𝕜 f s) s}
id                           └───────────────┘        └────────────────────┘   └───────────┘      
src                    └────┘└───────────────┘                           └───────────┘   └┘
typ                    └────┘└───────────────┘   └────────────────────┘ └───────────┘ └┘
doc                    └────┘└───────────────┘                            └───────────┘   └┘
txt                    └────┘                                                             └┘
par                    └────┘                                                             └┘
pid                                                                                      └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
304  
305  @[simp] lemma times_cont_diff_on_rec_zero :
doc    └──┘
306    times_cont_diff_on_rec 𝕜 0 f s ↔ continuous_on f s :=
id     └────────────────────┘       └───────────┘  
src    └────────────────────┘          └───────────┘
typ    └────────────────────┘       └───────────┘  
doc    └────────────────────┘           └───────────┘
307  by refl
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
308  
src  
typ  
doc  
txt  
par  
pid  
st   
309  @[simp] lemma times_cont_diff_on_rec_succ :
doc    └──┘
310    times_cont_diff_on_rec 𝕜 n.succ f s ↔
id     └────────────────────┘  └───┘   
src    └────────────────────┘    └───┘     
typ    └────────────────────┘  └───┘   
doc    └────────────────────┘
311    differentiable_on 𝕜 f s ∧ times_cont_diff_on_rec 𝕜 n (λx, fderiv_within 𝕜 f s x) s :=
id     └───────────────┘     └────────────────────┘       └───────────┘      
src    └───────────────┘        └────────────────────┘          └───────────┘
typ    └───────────────┘     └────────────────────┘       └───────────┘      
doc    └───────────────┘         └────────────────────┘          └───────────┘
312  by refl
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
313  
src  
typ  
doc  
txt  
par  
pid  
st   
314  lemma times_cont_diff_on_rec.of_succ (h : times_cont_diff_on_rec 𝕜 n.succ f s) :
id                                             └────────────────────┘  └───┘  
src                                            └────────────────────┘    └───┘
typ                                            └────────────────────┘  └───┘  
doc                                            └────────────────────┘
315    times_cont_diff_on_rec 𝕜 n f s :=
id     └────────────────────┘    
src    └────────────────────┘
typ    └────────────────────┘    
doc    └────────────────────┘
316  begin
st   └─────
317    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
318    induction n with n IH generalizing F,
id               
src    └────────┘ └───────────────────────┘
typ    └────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────┘
txt    └────────┘ └───────────────────────┘
par    └────────┘ └───────────────────────┘
pid              └───────┘└─────────────┘
st   ─────────────────────────────────────┘└─
319    { exact h.1.continuous_on },
id             
src      └────┘ └───────────────┘
typ      └────┘└───────────────┘
doc      └────┘ └───────────────┘
txt      └────┘ └───────────────┘
par      └────┘ └───────────────┘
pid            └─────────────┘└┘
st   ───┘└──────────────────────┘└┘
320    { rw times_cont_diff_on_rec_succ at h ⊢,
id          └─────────────────────────┘
src      └─┘└─────────────────────────┘└─────┘
typ      └─┘└─────────────────────────┘└─────┘
doc      └─┘                           └─────┘
txt      └─┘                           └─────┘
par      └─┘                           └─────┘
pid                                   └─────┘
st   ────────────────────────────────────────┘└─
321      exact ⟨h.1, IH h.2⟩ }
id                   └┘ 
src      └────┘  └──┘   └──┘
typ      └────┘  └──┘└┘└──┘
doc      └────┘  └──┘   └──┘
txt      └────┘  └──┘   └──┘
par      └────┘  └──┘   └──┘
pid             └──┘   └─┘
st   ───────────────────────┘└─
322  end
st   ──┘
323  
324  lemma times_cont_diff_on_rec.continuous_on_iterated_fderiv_within
325    (h : times_cont_diff_on_rec 𝕜 n f s) :
id          └────────────────────┘    
src         └────────────────────┘
typ         └────────────────────┘    
doc         └────────────────────┘
326    continuous_on (iterated_fderiv_within 𝕜 n f s) s :=
id     └───────────┘  └────────────────────┘      
src    └───────────┘  └────────────────────┘
typ    └───────────┘  └────────────────────┘      
doc    └───────────┘  └────────────────────┘
327  begin
st   └─────
328    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
329    induction n with n IH generalizing F f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
330    { exact h },
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───┘└──────┘└┘
331    { rw iterated_fderiv_within_succ,
id          └─────────────────────────┘
src      └─┘└─────────────────────────┘
typ      └─┘└─────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────────────────┘└─
332      exact IH (times_cont_diff_on_rec_succ.1 h).2 }
id             └┘  └─────────────────────────┘   
src      └────┘   └─────────────────────────┘└─┘ └──┘
typ      └────┘└┘ └─────────────────────────┘└─┘└──┘
doc      └────┘                              └─┘ └──┘
txt      └────┘                              └─┘ └──┘
par      └────┘                              └─┘ └──┘
pid                                         └─┘ └─┘
st   ────────────────────────────────────────────────┘└─
333  end
st   ──┘
334  
335  lemma times_cont_diff_on_rec.differentiable_on (h : times_cont_diff_on_rec 𝕜 (n+1) f s) :
id                                                       └────────────────────┘       
src                                                      └────────────────────┘     
typ                                                      └────────────────────┘       
doc                                                      └────────────────────┘
336    differentiable_on 𝕜 (iterated_fderiv_within 𝕜 n f s) s :=
id     └───────────────┘   └────────────────────┘      
src    └───────────────┘    └────────────────────┘
typ    └───────────────┘   └────────────────────┘      
doc    └───────────────┘    └────────────────────┘
337  begin
st   └─────
338    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
339    induction n with n IH generalizing F f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
340    { exact h.1 },
id             
src      └────┘ └─┘
typ      └────┘└─┘
doc      └────┘ └─┘
txt      └────┘ └─┘
par      └────┘ └─┘
pid            └─┘
st   ───┘└────────┘└┘
341    { rw iterated_fderiv_within_succ,
id          └─────────────────────────┘
src      └─┘└─────────────────────────┘
typ      └─┘└─────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────────────────┘└─
342      apply IH h.2 }
id             └┘ 
src      └────┘   └─┘
typ      └────┘└┘└─┘
doc      └────┘   └─┘
txt      └────┘   └─┘
par      └────┘   └─┘
pid              └─┘
st   ────────────────┘└─
343  end
st   ──┘
344  
345  lemma times_cont_diff_on_rec_univ :
346    times_cont_diff_on_rec 𝕜 n f univ ↔ times_cont_diff_rec 𝕜 n f :=
id     └────────────────────┘    └──┘  └─────────────────┘   
src    └────────────────────┘       └──┘  └─────────────────┘
typ    └────────────────────┘    └──┘  └─────────────────┘   
doc    └────────────────────┘              └─────────────────┘
347  begin
st   └─────
348    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
349    induction n with n IH generalizing F f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
350    { rw [times_cont_diff_on_rec_zero, times_cont_diff_rec_zero, continuous_iff_continuous_on_univ] },
id           └─────────────────────────┘  └──────────────────────┘  └───────────────────────────────┘
src      └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└───────────────────────────────┘└┘
typ      └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└───────────────────────────────┘└┘
doc      └──┘                           └┘                        └┘                                 └┘
txt      └──┘                           └┘                        └┘                                 └┘
par      └──┘                           └┘                        └┘                                 └┘
pid        └┘                           └┘                        └┘                                 
st   ───┘└─────────────────────────────┘└────────────────────────┘└─────────────────────────────────┘└┘
351    { rw [times_cont_diff_on_rec_succ, times_cont_diff_rec_succ, differentiable_on_univ, fderiv_within_univ, IH] }
id           └─────────────────────────┘  └──────────────────────┘  └────────────────────┘  └────────────────┘
src      └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└────────────────────┘└┘└────────────────┘└┘  └┘
typ      └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└────────────────────┘└┘└────────────────┘└┘└┘└┘
doc      └──┘                           └┘                        └┘                      └┘                  └┘  └┘
txt      └──┘                           └┘                        └┘                      └┘                  └┘  └┘
par      └──┘                           └┘                        └┘                      └┘                  └┘  └┘
pid        └┘                           └┘                        └┘                      └┘                  └┘  
st   ──────────────────────────────────┘└────────────────────────┘└──────────────────────┘└──────────────────┘└──┘└─
352  end
st   ──┘
353  
354  /--
355  A function is `C^n` on a set, for `n : with_top ℕ`, if its derivatives of order at most `n`
356  are all well defined and continuous.
357  -/
358  def times_cont_diff_on (𝕜 : Type w) [nondiscrete_normed_field 𝕜] (n : with_top ℕ)
id                                        └──────────────────────┘        └──────┘ 
src                                       └──────────────────────┘         └──────┘ 
typ                                       └──────────────────────┘        └──────┘ 
doc                                       └──────────────────────┘
359    {E F : Type u} [normed_group E] [normed_space 𝕜 E]
id                     └──────────┘    └──────────┘  
src                    └──────────┘     └──────────┘
typ                    └──────────┘    └──────────┘  
doc                    └──────────┘     └──────────┘
360    [normed_group F] [normed_space 𝕜 F] (f : E → F) (s : set E) :=
id      └──────────┘    └──────────┘                   └─┘ 
src     └──────────┘     └──────────┘                       └─┘
typ     └──────────┘    └──────────┘                   └─┘ 
doc     └──────────┘     └──────────┘
361  (∀m:ℕ, (m : with_top ℕ) ≤ n → continuous_on (iterated_fderiv_within 𝕜 m f s) s)
id             └──────┘       └───────────┘  └────────────────────┘      
src             └──────┘        └───────────┘  └────────────────────┘
typ            └──────┘       └───────────┘  └────────────────────┘      
doc                                └───────────┘  └────────────────────┘
362  ∧ (∀m:ℕ, (m : with_top ℕ) < n → differentiable_on 𝕜 (iterated_fderiv_within 𝕜 m f s) s)
id              └──────┘       └───────────────┘   └────────────────────┘      
src              └──────┘        └───────────────┘    └────────────────────┘
typ             └──────┘       └───────────────┘   └────────────────────┘      
doc                                  └───────────────┘    └────────────────────┘
363  
364  @[simp] lemma times_cont_diff_on_zero :
doc    └──┘
365    times_cont_diff_on 𝕜 0 f s ↔ continuous_on f s :=
id     └────────────────┘       └───────────┘  
src    └────────────────┘          └───────────┘
typ    └────────────────┘       └───────────┘  
doc    └────────────────┘           └───────────┘
366  by simp [times_cont_diff_on]
id            └────────────────┘
src     └────┘└────────────────┘└─
typ     └────┘└────────────────┘└─
doc     └────┘└────────────────┘└─
txt     └────┘                  └─
par     └────┘                  └─
pid                           
st     └──────────────────────────
367  
src  
typ  
doc  
txt  
par  
pid  
st   
368  /--
369  The two definitions of `C^n` functions on domains, directly in terms of continuity of all
370  derivatives, or by induction, are equivalent.
371  -/
372  theorem times_cont_diff_on_iff_times_cont_diff_on_rec :
373    times_cont_diff_on 𝕜 n f s ↔ times_cont_diff_on_rec 𝕜 n f s :=
id     └────────────────┘      └────────────────────┘    
src    └────────────────┘          └────────────────────┘
typ    └────────────────┘      └────────────────────┘    
doc    └────────────────┘           └────────────────────┘
374  begin
st   └─────
375    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
376    induction n with n IH generalizing F f,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
st   ───────────────────────────────────────┘└─
377    { rw [with_top.coe_zero, times_cont_diff_on_rec_zero, times_cont_diff_on_zero] },
id           └───────────────┘  └─────────────────────────┘  └─────────────────────┘
src      └──┘└───────────────┘└┘└─────────────────────────┘└┘└─────────────────────┘└┘
typ      └──┘└───────────────┘└┘└─────────────────────────┘└┘└─────────────────────┘└┘
doc      └──┘                 └┘                           └┘                       └┘
txt      └──┘                 └┘                           └┘                       └┘
par      └──┘                 └┘                           └┘                       └┘
pid        └┘                 └┘                           └┘                       
st   ───┘└───────────────────┘└───────────────────────────┘└───────────────────────┘└┘
378    { split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
379      { assume H,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────┘└──────┘└─
380        rw times_cont_diff_on_rec_succ,
id            └─────────────────────────┘
src        └─┘└─────────────────────────┘
typ        └─┘└─────────────────────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ───────────────────────────────────┘└─
381        refine ⟨H.2 0 (by simp only [with_top.zero_lt_coe, with_top.coe_zero, nat.succ_pos n]), _⟩,
id                                     └──────────────────┘  └───────────────┘  └──────────┘ 
src        └─────┘  └───┘   └─────────┘└──────────────────┘└┘└───────────────┘└┘└──────────┘ └───┘
typ        └─────┘ └───┘   └─────────┘└──────────────────┘└┘└───────────────┘└┘└──────────┘└───┘
doc        └─────┘  └───┘   └─────────┘                    └┘                 └┘             └───┘
txt        └─────┘  └───┘   └─────────┘                    └┘                 └┘             └───┘
par        └─────┘  └───┘   └─────────┘                    └┘                 └┘             └───┘
pid                └───┘   └──────────┘                    └┘                 └┘             └────┘
st   ──────────────────────┘└──────────────────────────────────────────────────────────────────┘└───┘└─
382        rw ← IH,
src        └───┘
typ        └───┘└┘
doc        └───┘
txt        └───┘
par        └───┘
pid          └─┘
st   ────────────┘└─
383        split,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
384        { assume m hm,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid          └─────────┘
st   ───────┘└─────────┘└─
385          have : (m.succ : with_top nat) ≤ n.succ :=
id                   └────┘   └──────┘ └─┘   └────┘
src          └─────┘ └────┘└─┘└──────┘└─┘└┘└────┘└───
typ          └─────┘ └────┘└─┘└──────┘└─┘└┘└────┘└───
doc          └─────┘       └─┘           └┘       └───
txt          └─────┘       └─┘           └┘       └───
par          └─────┘       └─┘           └┘       └───
pid          └───┘└┘       └─┘           └┘       └───
st   ───────────────────────────────────────────────────
386            with_top.coe_le_coe.2 (nat.succ_le_succ (with_top.coe_le_coe.1 hm)),
id                                    └──────────────┘  └─────────────────┘   └┘
src  ─────────┘                   └─┘ └──────────────┘ └─────────────────┘└─┘  └┘
typ  ─────────┘                   └─┘ └──────────────┘ └─────────────────┘└─┘└┘└┘
doc  ─────────┘                   └─┘                                     └─┘  └┘
txt  ─────────┘                   └─┘                                     └─┘  └┘
par  ─────────┘                   └─┘                                     └─┘  └┘
pid  ─────────┘                   └─┘                                     └─┘  └┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
387          exact H.1 _ this },
id                      └──┘
src          └────┘ └───┘    
typ          └────┘└───┘└──┘
doc          └────┘ └───┘    
txt          └────┘ └───┘    
par          └────┘ └───┘    
pid                └───┘    
st   ────────────────────────┘└┘
388        { assume m hm,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid          └─────────┘
st   ──────────────────┘└─
389          have : (m.succ : with_top nat) < n.succ :=
id                   └────┘   └──────┘ └─┘   └────┘
src          └─────┘ └────┘└─┘└──────┘└─┘└┘└────┘└───
typ          └─────┘ └────┘└─┘└──────┘└─┘└┘└────┘└───
doc          └─────┘       └─┘           └┘       └───
txt          └─────┘       └─┘           └┘       └───
par          └─────┘       └─┘           └┘       └───
pid          └───┘└┘       └─┘           └┘       └───
st   ───────────────────────────────────────────────────
390            with_top.coe_lt_coe.2 (nat.succ_le_succ (with_top.coe_lt_coe.1 hm)),
id                                    └──────────────┘  └─────────────────┘   └┘
src  ─────────┘                   └─┘ └──────────────┘ └─────────────────┘└─┘  └┘
typ  ─────────┘                   └─┘ └──────────────┘ └─────────────────┘└─┘└┘└┘
doc  ─────────┘                   └─┘                                     └─┘  └┘
txt  ─────────┘                   └─┘                                     └─┘  └┘
par  ─────────┘                   └─┘                                     └─┘  └┘
pid  ─────────┘                   └─┘                                     └─┘  └┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
391          exact H.2 _ this } },
id                      └──┘
src          └────┘ └───┘    
typ          └────┘└───┘└──┘
doc          └────┘ └───┘    
txt          └────┘ └───┘    
par          └────┘ └───┘    
pid                └───┘    
st   ────────────────────────┘└──┘
392      { assume H,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────────────┘└─
393        split,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
394        { assume m hm,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid          └─────────┘
st   ───────┘└─────────┘└─
395          simp only [with_top.coe_le_coe] at hm,
id                      └─────────────────┘
src          └─────────┘└─────────────────┘└─────┘
typ          └─────────┘└─────────────────┘└─────┘
doc          └─────────┘                   └─────┘
txt          └─────────┘                   └─────┘
par          └─────────┘                   └─────┘
pid              └──┘└┘                   └───┘
st   ────────────────────────────────────────────┘└─
396          cases nat.of_le_succ hm with h h,
id                 └────────────┘ └┘
src          └────┘└────────────┘  └───────┘
typ          └────┘└────────────┘└┘└───────┘
doc          └────┘                └───────┘
txt          └────┘                └───────┘
par          └────┘                └───────┘
pid                               └───────┘
st   ───────────────────────────────────────┘└─
397          { have := H.of_succ,
id                     └───────┘
src            └──────┘└───────┘
typ            └──────┘└───────┘
doc            └──────┘
txt            └──────┘
par            └──────┘
pid            └───┘└─┘
st   ─────────┘└───────────────┘└─
398            rw ← IH at this,
src            └───┘  └──────┘
typ            └───┘└┘└──────┘
doc            └───┘  └──────┘
txt            └───┘  └──────┘
par            └───┘  └──────┘
pid              └─┘  └──────┘
st   ────────────────────────┘└─
399            exact this.1 _ (with_top.coe_le_coe.2 h) },
id                   └──┘      └─────────────────┘   
src            └────┘    └───┘ └─────────────────┘└─┘ └┘
typ            └────┘└──┘└───┘ └─────────────────┘└─┘└┘
doc            └────┘    └───┘                    └─┘ └┘
txt            └────┘    └───┘                    └─┘ └┘
par            └────┘    └───┘                    └─┘ └┘
pid                     └───┘                    └─┘ 
st   ──────────────────────────────────────────────────┘└┘
400          { rw h,
id                
src            └─┘
typ            └─┘
doc            └─┘
txt            └─┘
par            └─┘
pid              
st   ─────────────┘└─
401            simp at H,
src            └───────┘
typ            └───────┘
doc            └───────┘
txt            └───────┘
par            └───────┘
pid                └──┘
st   ──────────────────┘└─
402            exact H.2.continuous_on_iterated_fderiv_within } },
id                   
src            └────┘ └──────────────────────────────────────┘
typ            └────┘└──────────────────────────────────────┘
doc            └────┘ └──────────────────────────────────────┘
txt            └────┘ └──────────────────────────────────────┘
par            └────┘ └──────────────────────────────────────┘
pid                  └────────────────────────────────────┘└┘
st   ────────────────────────────────────────────────────────┘└──┘
403        { assume m hm,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid          └─────────┘
st   ──────────────────┘└─
404          simp only [with_top.coe_lt_coe] at hm,
id                      └─────────────────┘
src          └─────────┘└─────────────────┘└─────┘
typ          └─────────┘└─────────────────┘└─────┘
doc          └─────────┘                   └─────┘
txt          └─────────┘                   └─────┘
par          └─────────┘                   └─────┘
pid              └──┘└┘                   └───┘
st   ────────────────────────────────────────────┘└─
405          cases nat.of_le_succ hm with h h,
id                 └────────────┘ └┘
src          └────┘└────────────┘  └───────┘
typ          └────┘└────────────┘└┘└───────┘
doc          └────┘                └───────┘
txt          └────┘                └───────┘
par          └────┘                └───────┘
pid                               └───────┘
st   ───────────────────────────────────────┘└─
406          { have := H.of_succ,
id                     └───────┘
src            └──────┘└───────┘
typ            └──────┘└───────┘
doc            └──────┘
txt            └──────┘
par            └──────┘
pid            └───┘└─┘
st   ─────────┘└───────────────┘└─
407            rw ← IH at this,
src            └───┘  └──────┘
typ            └───┘└┘└──────┘
doc            └───┘  └──────┘
txt            └───┘  └──────┘
par            └───┘  └──────┘
pid              └─┘  └──────┘
st   ────────────────────────┘└─
408            exact this.2 _ (with_top.coe_lt_coe.2 h) },
id                   └──┘      └─────────────────┘   
src            └────┘    └───┘ └─────────────────┘└─┘ └┘
typ            └────┘└──┘└───┘ └─────────────────┘└─┘└┘
doc            └────┘    └───┘                    └─┘ └┘
txt            └────┘    └───┘                    └─┘ └┘
par            └────┘    └───┘                    └─┘ └┘
pid                     └───┘                    └─┘ 
st   ──────────────────────────────────────────────────┘└┘
409          { rw nat.succ_inj h,
id                └──────────┘ 
src            └─┘└──────────┘
typ            └─┘└──────────┘
doc            └─┘            
txt            └─┘            
par            └─┘            
pid                          
st   ──────────────────────────┘└─
410            exact H.differentiable_on } } } },
id                   └─────────────────┘
src            └────┘└─────────────────┘
typ            └────┘└─────────────────┘
doc            └────┘                   
txt            └────┘                   
par            └────┘                   
pid                                    
st   ───────────────────────────────────┘└────────
411  end
st   ──┘
412  
413  /- Next lemma is marked as a simp lemma as `C^(n+1)` functions appear mostly in inductions. -/
414  @[simp] lemma times_cont_diff_on_succ :
doc    └──┘
415    times_cont_diff_on 𝕜 n.succ f s ↔
id     └────────────────┘  └───┘   
src    └────────────────┘    └───┘     
typ    └────────────────┘  └───┘   
doc    └────────────────┘
416    differentiable_on 𝕜 f s ∧ times_cont_diff_on 𝕜 n (λx, fderiv_within 𝕜 f s x) s :=
id     └───────────────┘     └────────────────┘       └───────────┘      
src    └───────────────┘        └────────────────┘          └───────────┘
typ    └───────────────┘     └────────────────┘       └───────────┘      
doc    └───────────────┘         └────────────────┘          └───────────┘
417  by simp [times_cont_diff_on_iff_times_cont_diff_on_rec]
id            └───────────────────────────────────────────┘
src     └────┘└───────────────────────────────────────────┘└─
typ     └────┘└───────────────────────────────────────────┘└─
doc     └────┘└───────────────────────────────────────────┘└─
txt     └────┘                                             └─
par     └────┘                                             └─
pid                                                      
st     └─────────────────────────────────────────────────────
418  
src  
typ  
doc  
txt  
par  
pid  
st   
419  lemma times_cont_diff_on.of_le {m n : with_top ℕ}
id                                         └──────┘ 
src                                        └──────┘ 
typ                                        └──────┘ 
420   (h : times_cont_diff_on 𝕜 n f s) (le : m ≤ n) : times_cont_diff_on 𝕜 m f s :=
id         └────────────────┘                  └────────────────┘    
src        └────────────────┘                        └────────────────┘
typ        └────────────────┘                  └────────────────┘    
doc        └────────────────┘                         └────────────────┘
421  ⟨λp hp, h.1 p (le_trans hp le), λp hp, h.2 p (lt_of_lt_of_le hp le)⟩
id      └┘      └──────┘ └┘ └┘     └┘      └────────────┘ └┘ └┘
src                └──────┘                      └────────────┘
typ     └┘      └──────┘ └┘ └┘     └┘      └────────────┘ └┘ └┘
422  
423  lemma times_cont_diff_on.of_succ (h : times_cont_diff_on 𝕜 n.succ f s) :
id                                         └────────────────┘  └───┘  
src                                        └────────────────┘    └───┘
typ                                        └────────────────┘  └───┘  
doc                                        └────────────────┘
424    times_cont_diff_on 𝕜 n f s :=
id     └────────────────┘    
src    └────────────────┘
typ    └────────────────┘    
doc    └────────────────┘
425  h.of_le (with_top.coe_le_coe.2 (nat.le_succ n))
id   └────┘  └─────────────────┘   └─────────┘ 
src   └────┘  └─────────────────┘   └─────────┘
typ  └────┘  └─────────────────┘   └─────────┘ 
426  
427  lemma times_cont_diff_on.continuous_on {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) :
id                                               └──────┘        └────────────────┘    
src                                              └──────┘        └────────────────┘
typ                                              └──────┘        └────────────────┘    
doc                                                               └────────────────┘
428    continuous_on f s :=
id     └───────────┘  
src    └───────────┘
typ    └───────────┘  
doc    └───────────┘
429  h.1 0 (by simp)
id   
src           └──┘
typ          └──┘
doc            └──┘
txt            └──┘
par            └──┘
st            └───┘
430  
431  lemma times_cont_diff_on.continuous_on_fderiv_within
432    {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) (hn : 1 ≤ n) :
id          └──────┘        └────────────────┘               
src         └──────┘        └────────────────┘                  
typ         └──────┘        └────────────────┘               
doc                          └────────────────┘
433    continuous_on (fderiv_within 𝕜 f s) s :=
id     └───────────┘  └───────────┘     
src    └───────────┘  └───────────┘
typ    └───────────┘  └───────────┘     
doc    └───────────┘  └───────────┘
434  h.1 1 hn
id       └┘
src   
typ      └┘
435  
436  /-- If a function is at least C^1 on a set, it is differentiable there. -/
437  lemma times_cont_diff_on.differentiable_on
438    {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) (hn : 1 ≤ n) :
id          └──────┘        └────────────────┘               
src         └──────┘        └────────────────┘                  
typ         └──────┘        └────────────────┘               
doc                          └────────────────┘
439    differentiable_on 𝕜 f s :=
id     └───────────────┘   
src    └───────────────┘
typ    └───────────────┘   
doc    └───────────────┘
440  begin
st   └─────
441    refine h.2 0 _,
id            
src    └─────┘ └────┘
typ    └─────┘└────┘
doc    └─────┘ └────┘
txt    └─────┘ └────┘
par    └─────┘ └────┘
pid           └────┘
st   ───────────────┘└─
442    refine lt_of_lt_of_le _ hn,
id            └────────────┘   └┘
src    └─────┘└────────────┘└─┘
typ    └─────┘└────────────┘└─┘└┘
doc    └─────┘              └─┘
txt    └─────┘              └─┘
par    └─────┘              └─┘
pid                        └─┘
st   ───────────────────────────┘└─
443    change ((0 : ℕ) : with_top ℕ) < (1 : ℕ),
id                       └──────┘    
src    └─────┘  └──┘ └──┘└──────┘ └┘ └──┘ 
typ    └─────┘  └──┘ └──┘└──────┘ └┘ └──┘ 
doc    └─────┘  └──┘ └──┘         └┘  └──┘ 
txt    └─────┘  └──┘ └──┘         └┘  └──┘ 
par    └─────┘  └──┘ └──┘         └┘  └──┘ 
pid            └──┘ └──┘         └┘  └──┘ 
st   ────────────────────────────────────────┘└─
444    rw with_top.coe_lt_coe,
id        └─────────────────┘
src    └─┘└─────────────────┘
typ    └─┘└─────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────┘└─
445    exact zero_lt_one
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ───────────────────┘
446  end
st   └─┘
447  
448  set_option class.instance_max_depth 50
doc             └──────────────────────┘
449  
450  /--
451  If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
452  continuous.
453  -/
454  lemma times_cont_diff_on.continuous_on_fderiv_within_apply
455    {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) (hn : 1 ≤ n) :
id          └──────┘        └────────────────┘               
src         └──────┘        └────────────────┘                  
typ         └──────┘        └────────────────┘               
doc                          └────────────────┘
456    continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1 : E → F) p.2) (set.prod s univ) :=
id     └───────────┘            └───────────┘                 └──────┘  └──┘
src    └───────────┘              └───────────┘                        └──────┘   └──┘
typ    └───────────┘            └───────────┘                 └──────┘  └──┘
doc    └───────────┘               └───────────┘                          └──────┘
457  begin
st   └─────
458    have A : continuous (λq : (E →L[𝕜] F) × E, q.1 q.2) := is_bounded_bilinear_map_apply.continuous,
id              └────────┘          └─┘                  └──────────────────────────────────────┘
src    └───────┘└────────┘  └──┘  └─┘  └┘ └┘ └─┘ └─────┘└──────────────────────────────────────┘
typ    └───────┘└────────┘  └──┘  └─┘└┘└┘ └─┘ └─────┘└──────────────────────────────────────┘
doc    └───────┘└────────┘  └──┘  └─┘  └┘  └┘ └─┘ └─────┘
txt    └───────┘            └──┘        └┘  └┘ └─┘ └─────┘
par    └───────┘            └──┘        └┘  └┘ └─┘ └─────┘
pid    └────┘└─┘            └──┘        └┘  └┘ └─┘ └─┘└──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
459    have B : continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1, p.2)) (set.prod s univ),
id              └───────────┘            └───────────┘                 └──────┘  └──┘
src    └───────┘└───────────┘  └──┘   └┘└───────────┘    └──┘ └───┘ └──────┘ └──┘
typ    └───────┘└───────────┘  └──┘ └┘└───────────┘  └──┘ └───┘ └──────┘└──┘
doc    └───────┘└───────────┘  └──┘   └┘ └───────────┘    └──┘ └───┘ └──────┘     
txt    └───────┘               └──┘   └┘                  └──┘ └───┘              
par    └───────┘               └──┘   └┘                  └──┘ └───┘              
pid    └────┘└─┘               └──┘   └┘                  └──┘ └───┘              
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
460    { apply continuous_on.prod _ continuous_snd.continuous_on,
id             └────────────────┘   └──────────────────────────┘
src      └────┘└────────────────┘└─┘└──────────────────────────┘
typ      └────┘└────────────────┘└─┘└──────────────────────────┘
doc      └────┘                  └─┘
txt      └────┘                  └─┘
par      └────┘                  └─┘
pid                             └─┘
st   ───┘└─────────────────────────────────────────────────────┘└─
461      exact continuous_on.comp (h.continuous_on_fderiv_within hn) continuous_fst.continuous_on
id             └────────────────┘  └───────────────────────────┘ └┘  └──────────────────────────┘
src      └────┘└────────────────┘ └───────────────────────────┘  └┘└──────────────────────────┘
typ      └────┘└────────────────┘ └───────────────────────────┘└┘└┘└──────────────────────────┘
doc      └────┘                                                  └┘                            
txt      └────┘                                                  └┘                            
par      └────┘                                                  └┘                            
pid                                                             └┘                            
st   ─────────────────────────────────────────────────────────────────────────────────────────────
462        (prod_subset_preimage_fst _ _) },
id          └──────────────────────┘
src  ─────┘ └──────────────────────┘└────┘
typ  ─────┘ └──────────────────────┘└────┘
doc  ─────┘                         └────┘
txt  ─────┘                         └────┘
par  ─────┘                         └────┘
pid  ─────┘                         └───┘
st   ────────────────────────────────────┘└┘
463    exact A.comp_continuous_on B
id           └──────────────────┘ 
src    └────┘└──────────────────┘ 
typ    └────┘└──────────────────┘
doc    └────┘                     
txt    └────┘                     
par    └────┘                     
pid                              
st   ──────────────────────────────┘
464  end
st   └─┘
465  
466  lemma times_cont_diff_on_top :
467    times_cont_diff_on 𝕜 ⊤ f s ↔ (∀n:ℕ, times_cont_diff_on 𝕜 n f s) :=
id     └────────────────┘            └────────────────┘    
src    └────────────────┘               └────────────────┘
typ    └────────────────┘            └────────────────┘    
doc    └────────────────┘                  └────────────────┘
468  begin
st   └─────
469    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
470    { assume h n,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid      └────────┘
st   ───┘└────────┘└─
471      exact h.of_le lattice.le_top },
id             └─────┘ └────────────┘
src      └────┘└─────┘└────────────┘
typ      └────┘└─────┘└────────────┘
doc      └────┘                     
txt      └────┘                     
par      └────┘                     
pid                                
st   ────────────────────────────────┘└┘
472    { assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
473      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
474      { exact λm hm, (h m).1 m (le_refl _) },
id                                └─────┘
src        └────┘ └────┘   └──┘  └─────┘└──┘
typ        └────┘ └────┘  └──┘  └─────┘└──┘
doc        └────┘ └────┘   └──┘         └──┘
txt        └────┘ └────┘   └──┘         └──┘
par        └────┘ └────┘   └──┘         └──┘
pid              └────┘   └──┘         └─┘
st   ─────┘└─────────────────────────────────┘└┘
475      { exact λ m hm, (h m.succ).2 m (with_top.coe_lt_coe.2 (lt_add_one m)) } }
id                          └───┘       └─────────────────┘    └────────┘
src        └────┘ └─────┘   └───┘└──┘  └─────────────────┘└─┘ └────────┘ └─┘
typ        └────┘ └─────┘  └───┘└──┘  └─────────────────┘└─┘ └────────┘ └─┘
doc        └────┘ └─────┘        └──┘                     └─┘            └─┘
txt        └────┘ └─────┘        └──┘                     └─┘            └─┘
par        └────┘ └─────┘        └──┘                     └─┘            └─┘
pid              └─────┘        └──┘                     └─┘            └┘
st   ─────────────────────────────────────────────────────────────────────────┘└───
476  end
st   ──┘
477  
478  lemma times_cont_diff_on_fderiv_within_nat {m n : ℕ}
id                                                     
src                                                    
typ                                                    
479    (hf : times_cont_diff_on 𝕜 n f s) (h : m + 1 ≤ n) :
id           └────────────────┘                
src          └────────────────┘                    
typ          └────────────────┘                
doc          └────────────────┘
480    times_cont_diff_on 𝕜 m (λx, fderiv_within 𝕜 f s x) s :=
id     └────────────────┘       └───────────┘      
src    └────────────────┘          └───────────┘
typ    └────────────────┘       └───────────┘      
doc    └────────────────┘          └───────────┘
481  begin
st   └─────
482    have : times_cont_diff_on 𝕜 m.succ f s :=
id            └────────────────┘  └────┘  
src    └─────┘└────────────────┘ └────┘  └───
typ    └─────┘└────────────────┘└────┘└───
doc    └─────┘└────────────────┘         └───
txt    └─────┘                           └───
par    └─────┘                           └───
pid    └───┘└┘                           └───
st   ────────────────────────────────────────────
483      hf.of_le (with_top.coe_le_coe.2 h),
id       └──────┘  └─────────────────┘   
src  ───┘└──────┘ └─────────────────┘└─┘ 
typ  ───┘└──────┘ └─────────────────┘└─┘
doc  ───┘                            └─┘ 
txt  ───┘                            └─┘ 
par  ───┘                            └─┘ 
pid  ───┘                            └─┘ 
st   ─────────────────────────────────────┘└─
484    exact (times_cont_diff_on_succ.1 this).2
id            └─────────────────────┘   └──┘
src    └────┘ └─────────────────────┘└─┘    └──┘
typ    └────┘ └─────────────────────┘└─┘└──┘└──┘
doc    └────┘                        └─┘    └──┘
txt    └────┘                        └─┘    └──┘
par    └────┘                        └─┘    └──┘
pid                                 └─┘    └─┘
st   ──────────────────────────────────────────┘
485  end
st   └─┘
486  
487  lemma times_cont_diff_on_fderiv_within {m n : with_top ℕ}
id                                                 └──────┘ 
src                                                └──────┘ 
typ                                                └──────┘ 
488    (hf : times_cont_diff_on 𝕜 n f s) (h : m + 1 ≤ n) :
id           └────────────────┘                
src          └────────────────┘                    
typ          └────────────────┘                
doc          └────────────────┘
489    times_cont_diff_on 𝕜 m (λx, fderiv_within 𝕜 f s x) s :=
id     └────────────────┘       └───────────┘      
src    └────────────────┘          └───────────┘
typ    └────────────────┘       └───────────┘      
doc    └────────────────┘          └───────────┘
490  begin
st   └─────
491    cases m,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
492    { change ⊤ + 1 ≤ n at h,
id                   
src      └─────┘└─┘ └───┘
typ      └─────┘└─┘└───┘
doc      └─────┘  └─┘  └───┘
txt      └─────┘  └─┘  └───┘
par      └─────┘  └─┘  └───┘
pid              └─┘  └──┘
st   ───┘└───────────────────┘└─
493      have : n = ⊤, by simpa using h,
id                                  
src      └─────┘       └──────────┘
typ      └─────┘      └──────────┘
doc      └─────┘        └──────────┘
txt      └─────┘        └──────────┘
par      └─────┘        └──────────┘
pid      └───┘└┘             └────┘
st   ───────────────┘                  └─
494      rw this at hf,
id          └──┘
src      └─┘    └────┘
typ      └─┘└──┘└────┘
doc      └─┘    └────┘
txt      └─┘    └────┘
par      └─┘    └────┘
pid            └────┘
st   ────────────────┘└─
495      change times_cont_diff_on 𝕜 ⊤ (λ (x : E), fderiv_within 𝕜 f s x) s,
id              └────────────────┘                └───────────┘        
src      └─────┘└────────────────┘    └────┘ └─┘└───────────┘    └┘
typ      └─────┘└────────────────┘    └────┘└─┘└───────────┘  └┘
doc      └─────┘└────────────────┘    └────┘ └─┘└───────────┘    └┘
txt      └─────┘                      └────┘ └─┘                 └┘
par      └─────┘                      └────┘ └─┘                 └┘
pid                                  └────┘ └─┘                 └┘
st   ─────────────────────────────────────────────────────────────────────┘└─
496      rw times_cont_diff_on_top at ⊢ hf,
id          └────────────────────┘
src      └─┘└────────────────────┘└──────┘
typ      └─┘└────────────────────┘└──────┘
doc      └─┘                      └──────┘
txt      └─┘                      └──────┘
par      └─┘                      └──────┘
pid                              └──────┘
st   ────────────────────────────────────┘└─
497      exact λm, times_cont_diff_on_fderiv_within_nat (hf (m + 1)) (le_refl _) },
id                 └──────────────────────────────────┘  └┘           └─────┘
src      └────┘ └─┘└──────────────────────────────────┘      └───┘ └─────┘└──┘
typ      └────┘ └─┘└──────────────────────────────────┘ └┘   └───┘ └─────┘└──┘
doc      └────┘ └─┘                                          └───┘        └──┘
txt      └────┘ └─┘                                          └───┘        └──┘
par      └────┘ └─┘                                          └───┘        └──┘
pid            └─┘                                          └───┘        └─┘
st   ───────────────────────────────────────────────────────────────────────────┘└┘
498    { have : times_cont_diff_on 𝕜 (m + 1) f s := hf.of_le h,
id              └────────────────┘              └──────┘ 
src      └─────┘└────────────────┘    └──┘  └──┘└──────┘
typ      └─────┘└────────────────┘  └──┘└──┘└──────┘
doc      └─────┘└────────────────┘    └──┘  └──┘        
txt      └─────┘                      └──┘  └──┘        
par      └─────┘                      └──┘  └──┘        
pid      └───┘└┘                      └──┘  └──┘        
st   ────────────────────────────────────────────────────────┘└─
499      exact times_cont_diff_on_fderiv_within_nat this (le_refl _) }
id             └──────────────────────────────────┘ └──┘  └─────┘
src      └────┘└──────────────────────────────────┘     └─────┘└──┘
typ      └────┘└──────────────────────────────────┘└──┘ └─────┘└──┘
doc      └────┘                                                └──┘
txt      └────┘                                                └──┘
par      └────┘                                                └──┘
pid                                                           └─┘
st   ───────────────────────────────────────────────────────────────┘└─
500  end
st   ──┘
501  
502  lemma times_cont_diff_on.congr_mono {n : with_top ℕ} (H : times_cont_diff_on 𝕜 n f s)
id                                            └──────┘        └────────────────┘    
src                                           └──────┘        └────────────────┘
typ                                           └──────┘        └────────────────┘    
doc                                                            └────────────────┘
503    (hs : unique_diff_on 𝕜 s₁) (h : ∀x ∈ s₁, f₁ x = f x) (h₁ : s₁ ⊆ s) :
id           └────────────┘  └┘           └┘  └┘            └┘  
src          └────────────┘                                         
typ          └────────────┘  └┘           └┘  └┘            └┘  
doc          └────────────┘
504    times_cont_diff_on 𝕜 n f₁ s₁ :=
id     └────────────────┘   └┘ └┘
src    └────────────────┘
typ    └────────────────┘   └┘ └┘
doc    └────────────────┘
505  begin
st   └─────
506    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
507    induction n using with_top.nat_induction with n IH Itop generalizing F,
id               
src    └────────┘ └─────────────────────────────────────────────────────────┘
typ    └────────┘└─────────────────────────────────────────────────────────┘
doc    └────────┘ └─────────────────────────────────────────────────────────┘
txt    └────────┘ └─────────────────────────────────────────────────────────┘
par    └────────┘ └─────────────────────────────────────────────────────────┘
pid              └───────────────────────────┘└─────────────┘└─────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
508    { rw times_cont_diff_on_zero at H ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└─────┘
typ      └─┘└─────────────────────┘└─────┘
doc      └─┘                       └─────┘
txt      └─┘                       └─────┘
par      └─┘                       └─────┘
pid                               └─────┘
st   ───┘└───────────────────────────────┘└─
509      exact continuous_on.congr_mono H h h₁ },
id             └──────────────────────┘   └┘
src      └────┘└──────────────────────┘    
typ      └────┘└──────────────────────┘└┘
doc      └────┘                            
txt      └────┘                            
par      └────┘                            
pid                                       
st   ─────────────────────────────────────────┘└┘
510    { rw times_cont_diff_on_succ at H ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└─────┘
typ      └─┘└─────────────────────┘└─────┘
doc      └─┘                       └─────┘
txt      └─┘                       └─────┘
par      └─┘                       └─────┘
pid                               └─────┘
st   ───┘└───────────────────────────────┘└─
511      refine ⟨differentiable_on.congr_mono H.1 h h₁, IH H.2 (λx hx, _)⟩,
id               └──────────────────────────┘      └┘  └┘ 
src      └─────┘ └──────────────────────────┘ └─┘   └┘   └─┘  └───────┘
typ      └─────┘ └──────────────────────────┘ └─┘└┘└┘└┘└─┘  └───────┘
doc      └─────┘                              └─┘   └┘   └─┘  └───────┘
txt      └─────┘                              └─┘   └┘   └─┘  └───────┘
par      └─────┘                              └─┘   └┘   └─┘  └───────┘
pid                                          └─┘   └┘   └─┘  └───────┘
st   ────────────────────────────────────────────────────────────────────┘└─
512      apply differentiable_within_at.fderiv_within_congr_mono
id             └───────────────────────────────────────────────┘
src      └────┘└───────────────────────────────────────────────┘
typ      └────┘└───────────────────────────────────────────────┘
doc      └────┘                                                 
txt      └────┘                                                 
par      └────┘                                                 
pid                                                            
st   ────────────────────────────────────────────────────────────
513        (H.1 x (h₁ hx)) h (h x hx) (hs x hx) h₁ },
id                                   └┘  └┘  └┘
src  ─────┘  └─┘      └─┘      └┘      └┘  
typ  ─────┘ └─┘      └─┘     └┘ └┘└┘└┘└┘
doc  ─────┘  └─┘      └─┘      └┘      └┘  
txt  ─────┘  └─┘      └─┘      └┘      └┘  
par  ─────┘  └─┘      └─┘      └┘      └┘  
pid  ─────┘  └─┘      └─┘      └┘      └┘  
st   ─────────────────────────────────────────────┘└┘
514    { rw times_cont_diff_on_top at H ⊢,
id          └────────────────────┘
src      └─┘└────────────────────┘└─────┘
typ      └─┘└────────────────────┘└─────┘
doc      └─┘                      └─────┘
txt      └─┘                      └─────┘
par      └─┘                      └─────┘
pid                              └─────┘
st   ───────────────────────────────────┘└─
515      assume n, exact Itop n (H n) h }
id                       └──┘       
src      └──────┘  └────┘        └┘ 
typ      └──────┘  └────┘└──┘  └┘
doc      └──────┘  └────┘        └┘ 
txt      └──────┘  └────┘        └┘ 
par      └──────┘  └────┘        └┘ 
pid      └──────┘               └┘ 
st   ───────────┘└─────────────────────┘└─
516  end
st   ──┘
517  
518  lemma times_cont_diff_on.congr {n : with_top ℕ} {s : set E} (H : times_cont_diff_on 𝕜 n f s)
id                                       └──────┘        └─┘        └────────────────┘    
src                                      └──────┘        └─┘         └────────────────┘
typ                                      └──────┘        └─┘        └────────────────┘    
doc                                                                   └────────────────┘
519    (hs : unique_diff_on 𝕜 s) (h : ∀x ∈ s, f₁ x = f x) :
id           └────────────┘               └┘    
src          └────────────┘                        
typ          └────────────┘               └┘    
doc          └────────────┘
520    times_cont_diff_on 𝕜 n f₁ s :=
id     └────────────────┘   └┘ 
src    └────────────────┘
typ    └────────────────┘   └┘ 
doc    └────────────────┘
521  times_cont_diff_on.congr_mono H hs h (subset.refl _)
id   └───────────────────────────┘  └┘   └─────────┘
src  └───────────────────────────┘         └─────────┘
typ  └───────────────────────────┘  └┘   └─────────┘
522  
523  lemma times_cont_diff_on.congr_mono' {n m : with_top ℕ} {s : set E} (H : times_cont_diff_on 𝕜 n f s)
id                                               └──────┘        └─┘        └────────────────┘    
src                                              └──────┘        └─┘         └────────────────┘
typ                                              └──────┘        └─┘        └────────────────┘    
doc                                                                           └────────────────┘
524    (hs : unique_diff_on 𝕜 s₁) (h : ∀x ∈ s₁, f₁ x = f x) (h₁ : s₁ ⊆ s) (le : m ≤ n) :
id           └────────────┘  └┘           └┘  └┘            └┘            
src          └────────────┘                                                     
typ          └────────────┘  └┘           └┘  └┘            └┘            
doc          └────────────┘
525    times_cont_diff_on 𝕜 m f₁ s₁ :=
id     └────────────────┘   └┘ └┘
src    └────────────────┘
typ    └────────────────┘   └┘ └┘
doc    └────────────────┘
526  times_cont_diff_on.of_le (H.congr_mono hs h h₁) le
id   └──────────────────────┘  └─────────┘ └┘  └┘  └┘
src  └──────────────────────┘   └─────────┘
typ  └──────────────────────┘  └─────────┘ └┘  └┘  └┘
527  
528  lemma times_cont_diff_on.mono {n : with_top ℕ} {s t : set E} (h : times_cont_diff_on 𝕜 n f t)
id                                      └──────┘          └─┘        └────────────────┘    
src                                     └──────┘          └─┘         └────────────────┘
typ                                     └──────┘          └─┘        └────────────────┘    
doc                                                                    └────────────────┘
529    (hst : s ⊆ t) (hs : unique_diff_on 𝕜 s) : times_cont_diff_on 𝕜 n f s :=
id                      └────────────┘      └────────────────┘    
src                       └────────────┘        └────────────────┘
typ                     └────────────┘      └────────────────┘    
doc                        └────────────┘        └────────────────┘
530  times_cont_diff_on.congr_mono h hs (λx hx, rfl) hst
id   └───────────────────────────┘  └┘    └┘  └─┘  └─┘
src  └───────────────────────────┘              └─┘
typ  └───────────────────────────┘  └┘    └┘  └─┘  └─┘
531  
532  /--
533  Being `C^n` is a local property.
534  -/
535  lemma times_cont_diff_on_of_locally_times_cont_diff_on {n : with_top ℕ} {s : set E}
id                                                               └──────┘        └─┘ 
src                                                              └──────┘        └─┘
typ                                                              └──────┘        └─┘ 
536    (hs : unique_diff_on 𝕜 s) (h : ∀x∈s, ∃u, is_open u ∧ x ∈ u ∧ times_cont_diff_on 𝕜 n f (s ∩ u)) :
id           └────────────┘              └─────┘       └────────────────┘       
src          └────────────┘                   └─────┘          └────────────────┘          
typ          └────────────┘              └─────┘       └────────────────┘       
doc          └────────────┘                     └─────┘             └────────────────┘
537    times_cont_diff_on 𝕜 n f s :=
id     └────────────────┘    
src    └────────────────┘
typ    └────────────────┘    
doc    └────────────────┘
538  begin
st   └─────
539    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
540    { assume m hm,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
541      apply continuous_on_of_locally_continuous_on (λx hx, _),
id             └────────────────────────────────────┘
src      └────┘└────────────────────────────────────┘  └──────┘
typ      └────┘└────────────────────────────────────┘  └──────┘
doc      └────┘                                        └──────┘
txt      └────┘                                        └──────┘
par      └────┘                                        └──────┘
pid                                                   └──────┘
st   ──────────────────────────────────────────────────────────┘└─
542      rcases h x hx with ⟨u, u_open, xu, hu⟩,
id                └┘
src      └─────┘    └───────────────────────┘
typ      └─────┘└┘└───────────────────────┘
doc      └─────┘    └───────────────────────┘
txt      └─────┘    └───────────────────────┘
par      └─────┘    └───────────────────────┘
pid                └───────────────────────┘
st   ─────────────────────────────────────────┘└─
543      refine ⟨u, u_open, xu,_⟩,
id                 └────┘  └┘
src      └─────┘  └┘      └┘  └─┘
typ      └─────┘ └┘└────┘└┘└┘└─┘
doc      └─────┘  └┘      └┘  └─┘
txt      └─────┘  └┘      └┘  └─┘
par      └─────┘  └┘      └┘  └─┘
pid              └┘      └┘  └─┘
st   ───────────────────────────┘└─
544      apply continuous_on.congr_mono (hu.1 m hm) (λy hy, _) (subset.refl _),
id             └──────────────────────┘  └┘    └┘              └─────────┘
src      └────┘└──────────────────────┘   └─┘   └┘  └───────┘ └─────────┘└─┘
typ      └────┘└──────────────────────┘ └┘└─┘└┘└┘  └───────┘ └─────────┘└─┘
doc      └────┘                           └─┘   └┘  └───────┘            └─┘
txt      └────┘                           └─┘   └┘  └───────┘            └─┘
par      └────┘                           └─┘   └┘  └───────┘            └─┘
pid                                      └─┘   └┘  └───────┘            └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
545      symmetry,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
st   ───────────┘└─
546      exact iterated_fderiv_within_inter_open hy.2 u_open hy.1 (hs.inter u_open) },
id             └───────────────────────────────┘             └┘    └──────┘ └────┘
src      └────┘└───────────────────────────────┘  └─┘        └─┘ └──────┘      └┘
typ      └────┘└───────────────────────────────┘  └─┘      └┘└─┘ └──────┘└────┘└┘
doc      └────┘└───────────────────────────────┘  └─┘        └─┘               └┘
txt      └────┘                                   └─┘        └─┘               └┘
par      └────┘                                   └─┘        └─┘               └┘
pid                                              └─┘        └─┘               
st   ──────────────────────────────────────────────────────────────────────────────┘└┘
547    { assume m hm,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
548      apply differentiable_on_of_locally_differentiable_on (λx hx, _),
id             └────────────────────────────────────────────┘
src      └────┘└────────────────────────────────────────────┘  └──────┘
typ      └────┘└────────────────────────────────────────────┘  └──────┘
doc      └────┘                                                └──────┘
txt      └────┘                                                └──────┘
par      └────┘                                                └──────┘
pid                                                           └──────┘
st   ──────────────────────────────────────────────────────────────────┘└─
549      rcases h x hx with ⟨u, u_open, xu, hu⟩,
id                └┘
src      └─────┘    └───────────────────────┘
typ      └─────┘└┘└───────────────────────┘
doc      └─────┘    └───────────────────────┘
txt      └─────┘    └───────────────────────┘
par      └─────┘    └───────────────────────┘
pid                └───────────────────────┘
st   ─────────────────────────────────────────┘└─
550      refine ⟨u, u_open, xu,_⟩,
id                 └────┘  └┘
src      └─────┘  └┘      └┘  └─┘
typ      └─────┘ └┘└────┘└┘└┘└─┘
doc      └─────┘  └┘      └┘  └─┘
txt      └─────┘  └┘      └┘  └─┘
par      └─────┘  └┘      └┘  └─┘
pid              └┘      └┘  └─┘
st   ───────────────────────────┘└─
551      apply differentiable_on.congr_mono (hu.2 m hm) (λy hy, _) (subset.refl _),
id             └──────────────────────────┘  └┘    └┘              └─────────┘
src      └────┘└──────────────────────────┘   └─┘   └┘  └───────┘ └─────────┘└─┘
typ      └────┘└──────────────────────────┘ └┘└─┘└┘└┘  └───────┘ └─────────┘└─┘
doc      └────┘                               └─┘   └┘  └───────┘            └─┘
txt      └────┘                               └─┘   └┘  └───────┘            └─┘
par      └────┘                               └─┘   └┘  └───────┘            └─┘
pid                                          └─┘   └┘  └───────┘            └─┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
552      symmetry,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
st   ───────────┘└─
553      exact iterated_fderiv_within_inter_open hy.2 u_open hy.1 (hs.inter u_open) }
id             └───────────────────────────────┘             └┘    └──────┘ └────┘
src      └────┘└───────────────────────────────┘  └─┘        └─┘ └──────┘      └┘
typ      └────┘└───────────────────────────────┘  └─┘      └┘└─┘ └──────┘└────┘└┘
doc      └────┘└───────────────────────────────┘  └─┘        └─┘               └┘
txt      └────┘                                   └─┘        └─┘               └┘
par      └────┘                                   └─┘        └─┘               └┘
pid                                              └─┘        └─┘               
st   ──────────────────────────────────────────────────────────────────────────────┘└─
554  end
st   ──┘
555  
556  /--
557  A function is `C^n`, for `n : with_top ℕ`, if its derivatives of order at most `n` are all well
558  defined and continuous.
559  -/
560  def times_cont_diff (𝕜 : Type w) [nondiscrete_normed_field 𝕜] (n : with_top ℕ)
id                                     └──────────────────────┘        └──────┘ 
src                                    └──────────────────────┘         └──────┘ 
typ                                    └──────────────────────┘        └──────┘ 
doc                                    └──────────────────────┘
561    {E F : Type u} [normed_group E] [normed_space 𝕜 E]
id                     └──────────┘    └──────────┘  
src                    └──────────┘     └──────────┘
typ                    └──────────┘    └──────────┘  
doc                    └──────────┘     └──────────┘
562    [normed_group F] [normed_space 𝕜 F] (f : E → F) :=
id      └──────────┘    └──────────┘            
src     └──────────┘     └──────────┘
typ     └──────────┘    └──────────┘            
doc     └──────────┘     └──────────┘
563  (∀m:ℕ, (m : with_top ℕ) ≤ n → continuous (iterated_fderiv 𝕜 m f ))
id             └──────┘       └────────┘  └─────────────┘   
src             └──────┘        └────────┘  └─────────────┘
typ            └──────┘       └────────┘  └─────────────┘   
doc                                └────────┘  └─────────────┘
564  ∧ (∀m:ℕ, (m : with_top ℕ) < n → differentiable 𝕜 (iterated_fderiv 𝕜 m f))
id              └──────┘       └────────────┘   └─────────────┘   
src              └──────┘        └────────────┘    └─────────────┘
typ             └──────┘       └────────────┘   └─────────────┘   
doc                                  └────────────┘    └─────────────┘
565  
566  lemma times_cont_diff_on_univ {n : with_top ℕ} :
id                                      └──────┘ 
src                                     └──────┘ 
typ                                     └──────┘ 
567    times_cont_diff_on 𝕜 n f univ ↔ times_cont_diff 𝕜 n f :=
id     └────────────────┘    └──┘  └─────────────┘   
src    └────────────────┘       └──┘  └─────────────┘
typ    └────────────────┘    └──┘  └─────────────┘   
doc    └────────────────┘              └─────────────┘
568  by simp [times_cont_diff_on, times_cont_diff, iterated_fderiv_within_univ,
id            └────────────────┘  └─────────────┘  └─────────────────────────┘
src     └────┘└────────────────┘└┘└─────────────┘└┘└─────────────────────────┘└─
typ     └────┘└────────────────┘└┘└─────────────┘└┘└─────────────────────────┘└─
doc     └────┘└────────────────┘└┘└─────────────┘└┘                           └─
txt     └────┘                  └┘               └┘                           └─
par     └────┘                  └┘               └┘                           └─
pid                           └┘               └┘                           └─
st     └────────────────────────────────────────────────────────────────────────
569          continuous_iff_continuous_on_univ, differentiable_on_univ]
id           └───────────────────────────────┘  └────────────────────┘
src  ───────┘└───────────────────────────────┘└┘└────────────────────┘└─
typ  ───────┘└───────────────────────────────┘└┘└────────────────────┘└─
doc  ───────┘                                 └┘                      └─
txt  ───────┘                                 └┘                      └─
par  ───────┘                                 └┘                      └─
pid  ───────┘                                 └┘                      
st   ───────────────────────────────────────────────────────────────────
570  
src  
typ  
doc  
txt  
par  
pid  
st   
571  @[simp] lemma times_cont_diff_zero :
doc    └──┘
572    times_cont_diff 𝕜 0 f ↔ continuous f :=
id     └─────────────┘      └────────┘ 
src    └─────────────┘        └────────┘
typ    └─────────────┘      └────────┘ 
doc    └─────────────┘         └────────┘
573  by simp [times_cont_diff]
id            └─────────────┘
src     └────┘└─────────────┘└─
typ     └────┘└─────────────┘└─
doc     └────┘└─────────────┘└─
txt     └────┘               └─
par     └────┘               └─
pid                        
st     └───────────────────────
574  
src  
typ  
doc  
txt  
par  
pid  
st   
575  theorem times_cont_diff_iff_times_cont_diff_rec :
576    times_cont_diff 𝕜 n f ↔ times_cont_diff_rec 𝕜 n f :=
id     └─────────────┘     └─────────────────┘   
src    └─────────────┘        └─────────────────┘
typ    └─────────────┘     └─────────────────┘   
doc    └─────────────┘         └─────────────────┘
577  by simp [times_cont_diff_on_univ.symm, times_cont_diff_on_rec_univ.symm,
src     └────┘                            └┘                                └─
typ     └────┘└──────────────────────────┘└┘└──────────────────────────────┘└─
doc     └────┘                            └┘                                └─
txt     └────┘                            └┘                                └─
par     └────┘                            └┘                                └─
pid                                     └┘                                └─
st     └──────────────────────────────────────────────────────────────────────
578           times_cont_diff_on_iff_times_cont_diff_on_rec]
id            └───────────────────────────────────────────┘
src  ────────┘└───────────────────────────────────────────┘└─
typ  ────────┘└───────────────────────────────────────────┘└─
doc  ────────┘└───────────────────────────────────────────┘└─
txt  ────────┘                                             └─
par  ────────┘                                             └─
pid  ────────┘                                             
st   ────────────────────────────────────────────────────────
579  
src  
typ  
doc  
txt  
par  
pid  
st   
580  @[simp] lemma times_cont_diff_succ :
doc    └──┘
581    times_cont_diff 𝕜 n.succ f ↔
id     └─────────────┘  └───┘  
src    └─────────────┘    └───┘   
typ    └─────────────┘  └───┘  
doc    └─────────────┘
582    differentiable 𝕜 f ∧ times_cont_diff 𝕜 n (λx, fderiv 𝕜 f x) :=
id     └────────────┘    └─────────────┘       └────┘   
src    └────────────┘      └─────────────┘          └────┘
typ    └────────────┘    └─────────────┘       └────┘   
doc    └────────────┘       └─────────────┘          └────┘
583  by simp [times_cont_diff_iff_times_cont_diff_rec]
id            └─────────────────────────────────────┘
src     └────┘└─────────────────────────────────────┘└─
typ     └────┘└─────────────────────────────────────┘└─
doc     └────┘                                       └─
txt     └────┘                                       └─
par     └────┘                                       └─
pid                                                
st     └───────────────────────────────────────────────
584  
src  
typ  
doc  
txt  
par  
pid  
st   
585  lemma times_cont_diff.of_le {m n : with_top ℕ} (h : times_cont_diff 𝕜 n f) (le : m ≤ n) :
id                                      └──────┘        └─────────────┘             
src                                     └──────┘        └─────────────┘                
typ                                     └──────┘        └─────────────┘             
doc                                                      └─────────────┘
586    times_cont_diff 𝕜 m f :=
id     └─────────────┘   
src    └─────────────┘
typ    └─────────────┘   
doc    └─────────────┘
587  ⟨λp hp, h.1 p (le_trans hp le), λp hp, h.2 p (lt_of_lt_of_le hp le)⟩
id      └┘      └──────┘ └┘ └┘     └┘      └────────────┘ └┘ └┘
src                └──────┘                      └────────────┘
typ     └┘      └──────┘ └┘ └┘     └┘      └────────────┘ └┘ └┘
588  
589  lemma times_cont_diff.of_succ (h : times_cont_diff 𝕜 n.succ f) : times_cont_diff 𝕜 n f :=
id                                      └─────────────┘  └───┘     └─────────────┘   
src                                     └─────────────┘    └───┘      └─────────────┘
typ                                     └─────────────┘  └───┘     └─────────────┘   
doc                                     └─────────────┘               └─────────────┘
590  h.of_le (with_top.coe_le_coe.2 (nat.le_succ n))
id   └────┘  └─────────────────┘   └─────────┘ 
src   └────┘  └─────────────────┘   └─────────┘
typ  └────┘  └─────────────────┘   └─────────┘ 
591  
592  lemma times_cont_diff.continuous {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) :
id                                         └──────┘        └─────────────┘   
src                                        └──────┘        └─────────────┘
typ                                        └──────┘        └─────────────┘   
doc                                                         └─────────────┘
593    continuous f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
594  h.1 0 (by simp)
id   
src           └──┘
typ          └──┘
doc            └──┘
txt            └──┘
par            └──┘
st            └───┘
595  
596  lemma times_cont_diff.continuous_fderiv {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) (hn : 1 ≤ n) :
id                                                └──────┘        └─────────────┘              
src                                               └──────┘        └─────────────┘                
typ                                               └──────┘        └─────────────┘              
doc                                                                └─────────────┘
597    continuous (fderiv 𝕜 f) :=
id     └────────┘  └────┘  
src    └────────┘  └────┘
typ    └────────┘  └────┘  
doc    └────────┘  └────┘
598  h.1 1 hn
id       └┘
src   
typ      └┘
599  
600  lemma times_cont_diff.continuous_fderiv_apply
601    {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) (hn : 1 ≤ n) :
id          └──────┘        └─────────────┘              
src         └──────┘        └─────────────┘                
typ         └──────┘        └─────────────┘              
doc                          └─────────────┘
602    continuous (λp : E × E, (fderiv 𝕜 f p.1 : E → F) p.2) :=
id     └────────┘            └────┘            
src    └────────┘              └────┘                  
typ    └────────┘            └────┘            
doc    └────────┘               └────┘
603  begin
st   └─────
604    have A : continuous (λq : (E →L[𝕜] F) × E, q.1 q.2) := is_bounded_bilinear_map_apply.continuous,
id              └────────┘          └─┘                  └──────────────────────────────────────┘
src    └───────┘└────────┘  └──┘  └─┘  └┘ └┘ └─┘ └─────┘└──────────────────────────────────────┘
typ    └───────┘└────────┘  └──┘  └─┘└┘└┘ └─┘ └─────┘└──────────────────────────────────────┘
doc    └───────┘└────────┘  └──┘  └─┘  └┘  └┘ └─┘ └─────┘
txt    └───────┘            └──┘        └┘  └┘ └─┘ └─────┘
par    └───────┘            └──┘        └┘  └┘ └─┘ └─────┘
pid    └────┘└─┘            └──┘        └┘  └┘ └─┘ └─┘└──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
605    have B : continuous (λp : E × E, (fderiv 𝕜 f p.1, p.2)),
id              └────────┘            └────┘  
src    └───────┘└────────┘  └──┘   └┘└────┘   └──┘ └──┘
typ    └───────┘└────────┘  └──┘ └┘└────┘ └──┘ └──┘
doc    └───────┘└────────┘  └──┘   └┘ └────┘   └──┘ └──┘
txt    └───────┘            └──┘   └┘          └──┘ └──┘
par    └───────┘            └──┘   └┘          └──┘ └──┘
pid    └────┘└─┘            └──┘   └┘          └──┘ └──┘
st   ────────────────────────────────────────────────────────┘└─
606    { apply continuous.prod_mk _ continuous_snd,
id             └────────────────┘   └────────────┘
src      └────┘└────────────────┘└─┘└────────────┘
typ      └────┘└────────────────┘└─┘└────────────┘
doc      └────┘                  └─┘
txt      └────┘                  └─┘
par      └────┘                  └─┘
pid                             └─┘
st   ───┘└───────────────────────────────────────┘└─
607      exact continuous.comp (h.continuous_fderiv hn) continuous_fst },
id             └─────────────┘  └─────────────────┘ └┘  └────────────┘
src      └────┘└─────────────┘ └─────────────────┘  └┘└────────────┘
typ      └────┘└─────────────┘ └─────────────────┘└┘└┘└────────────┘
doc      └────┘                                     └┘              
txt      └────┘                                     └┘              
par      └────┘                                     └┘              
pid                                                └┘              
st   ─────────────────────────────────────────────────────────────────┘└┘
608    exact A.comp B
id           └────┘ 
src    └────┘└────┘ 
typ    └────┘└────┘
doc    └────┘       
txt    └────┘       
par    └────┘       
pid                
st   ────────────────┘
609  end
st   └─┘
610  
611  lemma times_cont_diff_top : times_cont_diff 𝕜 ⊤ f ↔ (∀n:ℕ, times_cont_diff 𝕜 n f) :=
id                               └─────────────┘           └─────────────┘   
src                              └─────────────┘             └─────────────┘
typ                              └─────────────┘           └─────────────┘   
doc                              └─────────────┘                └─────────────┘
612  by simp [times_cont_diff_on_univ.symm, times_cont_diff_on_rec_univ.symm,
src     └────┘                            └┘                                └─
typ     └────┘└──────────────────────────┘└┘└──────────────────────────────┘└─
doc     └────┘                            └┘                                └─
txt     └────┘                            └┘                                └─
par     └────┘                            └┘                                └─
pid                                     └┘                                └─
st     └──────────────────────────────────────────────────────────────────────
613          times_cont_diff_on_top]
id           └────────────────────┘
src  ───────┘└────────────────────┘└─
typ  ───────┘└────────────────────┘└─
doc  ───────┘                      └─
txt  ───────┘                      └─
par  ───────┘                      └─
pid  ───────┘                      
st   ────────────────────────────────
614  
src  
typ  
doc  
txt  
par  
pid  
st   
615  lemma times_cont_diff.times_cont_diff_on {n : with_top ℕ} {s : set E}
id                                                 └──────┘        └─┘ 
src                                                └──────┘        └─┘
typ                                                └──────┘        └─┘ 
616    (h : times_cont_diff 𝕜 n f) (hs : unique_diff_on 𝕜 s) : times_cont_diff_on 𝕜 n f s :=
id          └─────────────┘           └────────────┘      └────────────────┘    
src         └─────────────┘              └────────────┘        └────────────────┘
typ         └─────────────┘           └────────────┘      └────────────────┘    
doc         └─────────────┘              └────────────┘        └────────────────┘
617  by { rw ← times_cont_diff_on_univ at h, apply times_cont_diff_on.mono h (subset_univ _) hs }
id             └─────────────────────┘             └─────────────────────┘   └─────────┘    └┘
src       └───┘└─────────────────────┘└───┘  └────┘└─────────────────────┘  └─────────┘└──┘  
typ       └───┘└─────────────────────┘└───┘  └────┘└─────────────────────┘ └─────────┘└──┘└┘
doc       └───┘                       └───┘  └────┘                                    └──┘  
txt       └───┘                       └───┘  └────┘                                    └──┘  
par       └───┘                       └───┘  └────┘                                    └──┘  
pid         └─┘                       └───┘                                           └──┘  
st     └──────────────────────────────────┘└───────────────────────────────────────────────────┘└┘
618  
619  /--
620  Constants are C^∞.
621  -/
622  lemma times_cont_diff_const {n : with_top ℕ} {c : F} : times_cont_diff 𝕜 n (λx : E, c) :=
id                                    └──────┘            └─────────────┘           
src                                   └──────┘             └─────────────┘
typ                                   └──────┘            └─────────────┘           
doc                                                         └─────────────┘
623  begin
st   └─────
624    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
625    induction n using with_top.nat_induction with n IH Itop generalizing F,
id               
src    └────────┘ └─────────────────────────────────────────────────────────┘
typ    └────────┘└─────────────────────────────────────────────────────────┘
doc    └────────┘ └─────────────────────────────────────────────────────────┘
txt    └────────┘ └─────────────────────────────────────────────────────────┘
par    └────────┘ └─────────────────────────────────────────────────────────┘
pid              └───────────────────────────┘└─────────────┘└─────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
626    { rw times_cont_diff_zero,
id          └──────────────────┘
src      └─┘└──────────────────┘
typ      └─┘└──────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└─────────────────────┘└─
627      apply continuous_const },
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘                
txt      └────┘                
par      └────┘                
pid                           
st   ──────────────────────────┘└┘
628    { refine times_cont_diff_succ.2 ⟨differentiable_const _, _⟩,
id              └──────────────────┘    └──────────────────┘
src      └─────┘└──────────────────┘└─┘ └──────────────────┘└────┘
typ      └─────┘└──────────────────┘└─┘ └──────────────────┘└────┘
doc      └─────┘                    └─┘                     └────┘
txt      └─────┘                    └─┘                     └────┘
par      └─────┘                    └─┘                     └────┘
pid                                └─┘                     └────┘
st   ───┘└───────────────────────────────────────────────────────┘└─
629      simp [fderiv_const],
id             └──────────┘
src      └────┘└──────────┘
typ      └────┘└──────────┘
doc      └────┘            
txt      └────┘            
par      └────┘            
pid                      
st   ──────────────────────┘└─
630      exact IH },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ────────────┘└┘
631    { rw times_cont_diff_top,
id          └─────────────────┘
src      └─┘└─────────────────┘
typ      └─┘└─────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────────┘└─
632      assume n, apply Itop }
src      └──────┘  └────┘    
typ      └──────┘  └────┘    
doc      └──────┘  └────┘    
txt      └──────┘  └────┘    
par      └──────┘  └────┘    
pid      └──────┘           
st   ───────────┘└───────────┘└─
633  end
st   ──┘
634  
635  lemma times_cont_diff_on_const {n : with_top ℕ} {c : F} {s : set E} (hs : unique_diff_on 𝕜 s) :
id                                       └──────┘               └─┘         └────────────┘  
src                                      └──────┘                └─┘          └────────────┘
typ                                      └──────┘               └─┘         └────────────┘  
doc                                                                            └────────────┘
636    times_cont_diff_on 𝕜 n (λx : E, c) s :=
id     └────────────────┘             
src    └────────────────┘
typ    └────────────────┘             
doc    └────────────────┘
637  times_cont_diff_const.times_cont_diff_on hs
id   └───────────────────┘└─────────────────┘ └┘
src  └───────────────────┘└─────────────────┘
typ  └───────────────────┘└─────────────────┘ └┘
doc  └───────────────────┘
638  
639  /--
640  Linear functions are C^∞.
641  -/
642  lemma is_bounded_linear_map.times_cont_diff {n : with_top ℕ} (hf : is_bounded_linear_map 𝕜 f) :
id                                                    └──────┘         └───────────────────┘  
src                                                   └──────┘         └───────────────────┘
typ                                                   └──────┘         └───────────────────┘  
doc                                                                     └───────────────────┘
643    times_cont_diff 𝕜 n f :=
id     └─────────────┘   
src    └─────────────┘
typ    └─────────────┘   
doc    └─────────────┘
644  begin
st   └─────
645    induction n using with_top.nat_induction with n IH Itop,
id               
src    └────────┘ └──────────────────────────────────────────┘
typ    └────────┘└──────────────────────────────────────────┘
doc    └────────┘ └──────────────────────────────────────────┘
txt    └────────┘ └──────────────────────────────────────────┘
par    └────────┘ └──────────────────────────────────────────┘
pid              └───────────────────────────┘└─────────────┘
st   ────────────────────────────────────────────────────────┘└─
646    { rw times_cont_diff_zero,
id          └──────────────────┘
src      └─┘└──────────────────┘
typ      └─┘└──────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└─────────────────────┘└─
647      exact hf.continuous },
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘             
txt      └────┘             
par      └────┘             
pid                        
st   ───────────────────────┘└┘
648    { refine times_cont_diff_succ.2 ⟨hf.differentiable, _⟩,
id              └──────────────────┘    └───────────────┘
src      └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
typ      └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
doc      └─────┘                    └─┘                  └──┘
txt      └─────┘                    └─┘                  └──┘
par      └─────┘                    └─┘                  └──┘
pid                                └─┘                  └──┘
st   ───┘└──────────────────────────────────────────────────┘└─
649      simp [hf.fderiv],
src      └────┘         
typ      └────┘└───────┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                   
st   ───────────────────┘└─
650      exact times_cont_diff_const },
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘└───────────────────┘
txt      └────┘                     
par      └────┘                     
pid                                
st   ───────────────────────────────┘└┘
651    { rw times_cont_diff_top, apply Itop }
id          └─────────────────┘
src      └─┘└─────────────────┘  └────┘    
typ      └─┘└─────────────────┘  └────┘    
doc      └─┘                     └────┘    
txt      └─┘                     └────┘    
par      └─┘                     └────┘    
pid                                      
st   ─────────────────────────┘└───────────┘└─
652  end
st   ──┘
653  
654  /--
655  The first projection in a product is C^∞.
656  -/
657  lemma times_cont_diff_fst {n : with_top ℕ} : times_cont_diff 𝕜 n (prod.fst : E × F → E) :=
id                                  └──────┘     └─────────────┘    └──────┘        
src                                 └──────┘     └─────────────┘      └──────┘     
typ                                 └──────┘     └─────────────┘    └──────┘        
doc                                               └─────────────┘
658  is_bounded_linear_map.times_cont_diff is_bounded_linear_map.fst
id   └───────────────────────────────────┘ └───────────────────────┘
src  └───────────────────────────────────┘ └───────────────────────┘
typ  └───────────────────────────────────┘ └───────────────────────┘
doc  └───────────────────────────────────┘
659  
660  /--
661  The second projection in a product is C^∞.
662  -/
663  lemma times_cont_diff_snd {n : with_top ℕ} : times_cont_diff 𝕜 n (prod.snd : E × F → F) :=
id                                  └──────┘     └─────────────┘    └──────┘        
src                                 └──────┘     └─────────────┘      └──────┘     
typ                                 └──────┘     └─────────────┘    └──────┘        
doc                                               └─────────────┘
664  is_bounded_linear_map.times_cont_diff is_bounded_linear_map.snd
id   └───────────────────────────────────┘ └───────────────────────┘
src  └───────────────────────────────────┘ └───────────────────────┘
typ  └───────────────────────────────────┘ └───────────────────────┘
doc  └───────────────────────────────────┘
665  
666  /--
667  The identity is C^∞.
668  -/
669  lemma times_cont_diff_id {n : with_top ℕ} : times_cont_diff 𝕜 n (id : E → E) :=
id                                 └──────┘     └─────────────┘    └┘      
src                                └──────┘     └─────────────┘      └┘
typ                                └──────┘     └─────────────┘    └┘      
doc                                              └─────────────┘
670  is_bounded_linear_map.id.times_cont_diff
id   └──────────────────────┘└──────────────┘
src  └──────────────────────┘└──────────────┘
typ  └──────────────────────┘└──────────────┘
doc                          └──────────────┘
671  
672  /--
673  Bilinear functions are C^∞.
674  -/
675  lemma is_bounded_bilinear_map.times_cont_diff {n : with_top ℕ} (hb : is_bounded_bilinear_map 𝕜 b) :
id                                                      └──────┘         └─────────────────────┘  
src                                                     └──────┘         └─────────────────────┘
typ                                                     └──────┘         └─────────────────────┘  
doc                                                                       └─────────────────────┘
676    times_cont_diff 𝕜 n b :=
id     └─────────────┘   
src    └─────────────┘
typ    └─────────────┘   
doc    └─────────────┘
677  begin
st   └─────
678    induction n using with_top.nat_induction with n IH Itop,
id               
src    └────────┘ └──────────────────────────────────────────┘
typ    └────────┘└──────────────────────────────────────────┘
doc    └────────┘ └──────────────────────────────────────────┘
txt    └────────┘ └──────────────────────────────────────────┘
par    └────────┘ └──────────────────────────────────────────┘
pid              └───────────────────────────┘└─────────────┘
st   ────────────────────────────────────────────────────────┘└─
679    { rw times_cont_diff_zero,
id          └──────────────────┘
src      └─┘└──────────────────┘
typ      └─┘└──────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└─────────────────────┘└─
680      exact hb.continuous },
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘             
txt      └────┘             
par      └────┘             
pid                        
st   ───────────────────────┘└┘
681    { refine times_cont_diff_succ.2 ⟨hb.differentiable, _⟩,
id              └──────────────────┘    └───────────────┘
src      └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
typ      └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
doc      └─────┘                    └─┘                  └──┘
txt      └─────┘                    └─┘                  └──┘
par      └─────┘                    └─┘                  └──┘
pid                                └─┘                  └──┘
st   ───┘└──────────────────────────────────────────────────┘└─
682      simp [hb.fderiv],
src      └────┘         
typ      └────┘└───────┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                   
st   ───────────────────┘└─
683      exact hb.is_bounded_linear_map_deriv.times_cont_diff },
id             └────────────────────────────────────────────┘
src      └────┘└────────────────────────────────────────────┘
typ      └────┘└────────────────────────────────────────────┘
doc      └────┘└────────────────────────────────────────────┘
txt      └────┘                                              
par      └────┘                                              
pid                                                         
st   ────────────────────────────────────────────────────────┘└┘
684    { rw times_cont_diff_top, apply Itop }
id          └─────────────────┘
src      └─┘└─────────────────┘  └────┘    
typ      └─┘└─────────────────┘  └────┘    
doc      └─┘                     └────┘    
txt      └─┘                     └────┘    
par      └─┘                     └────┘    
pid                                      
st   ─────────────────────────┘└───────────┘└─
685  end
st   ──┘
686  
687  /--
688  Composition by bounded linear maps preserves `C^n` functions on domains.
689  -/
690  lemma times_cont_diff_on.comp_is_bounded_linear {n : with_top ℕ} {s : set E} {f : E → F} {g : F → G}
id                                                        └──────┘        └─┘                     
src                                                       └──────┘        └─┘
typ                                                       └──────┘        └─┘                     
691    (hf : times_cont_diff_on 𝕜 n f s) (hg : is_bounded_linear_map 𝕜 g) (hs : unique_diff_on 𝕜 s) :
id           └────────────────┘            └───────────────────┘          └────────────┘  
src          └────────────────┘                └───────────────────┘            └────────────┘
typ          └────────────────┘            └───────────────────┘          └────────────┘  
doc          └────────────────┘                └───────────────────┘            └────────────┘
692    times_cont_diff_on 𝕜 n (λx, g (f x)) s :=
id     └────────────────┘             
src    └────────────────┘
typ    └────────────────┘             
doc    └────────────────┘
693  begin
st   └─────
694    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
695    induction n using with_top.nat_induction with n IH Itop generalizing F G,
id               
src    └────────┘ └───────────────────────────────────────────────────────────┘
typ    └────────┘└───────────────────────────────────────────────────────────┘
doc    └────────┘ └───────────────────────────────────────────────────────────┘
txt    └────────┘ └───────────────────────────────────────────────────────────┘
par    └────────┘ └───────────────────────────────────────────────────────────┘
pid              └───────────────────────────┘└─────────────┘└───────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
696    { have : continuous_on g univ := hg.continuous.continuous_on,
id              └───────────┘  └──┘    └─────────────────────────┘
src      └─────┘└───────────┘ └──┘└──┘└─────────────────────────┘
typ      └─────┘└───────────┘└──┘└──┘└─────────────────────────┘
doc      └─────┘└───────────┘     └──┘
txt      └─────┘                  └──┘
par      └─────┘                  └──┘
pid      └───┘└┘                  └──┘
st   ───┘└────────────────────────────────────────────────────────┘└─
697      rw times_cont_diff_on_zero at hf ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└──────┘
typ      └─┘└─────────────────────┘└──────┘
doc      └─┘                       └──────┘
txt      └─┘                       └──────┘
par      └─┘                       └──────┘
pid                               └──────┘
st   ─────────────────────────────────────┘└─
698      apply continuous_on.comp this hf (subset_univ _) },
id             └────────────────┘ └──┘ └┘  └─────────┘
src      └────┘└────────────────┘       └─────────┘└──┘
typ      └────┘└────────────────┘└──┘└┘ └─────────┘└──┘
doc      └────┘                                    └──┘
txt      └────┘                                    └──┘
par      └────┘                                    └──┘
pid                                               └─┘
st   ────────────────────────────────────────────────────┘└┘
699    { rw times_cont_diff_on_succ at hf ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└──────┘
typ      └─┘└─────────────────────┘└──────┘
doc      └─┘                       └──────┘
txt      └─┘                       └──────┘
par      └─┘                       └──────┘
pid                               └──────┘
st   ───┘└────────────────────────────────┘└─
700      refine ⟨differentiable_on.comp hg.differentiable_on hf.1 subset_preimage_univ, _⟩,
id               └────────────────────┘ └──────────────────┘ └┘   └──────────────────┘
src      └─────┘ └────────────────────┘└──────────────────┘  └─┘└──────────────────┘└──┘
typ      └─────┘ └────────────────────┘└──────────────────┘└┘└─┘└──────────────────┘└──┘
doc      └─────┘                                             └─┘                    └──┘
txt      └─────┘                                             └─┘                    └──┘
par      └─────┘                                             └─┘                    └──┘
pid                                                         └─┘                    └──┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
701      let Φ : (E →L[𝕜] F) → (E →L[𝕜] G) := λu, continuous_linear_map.comp (hg.to_continuous_linear_map) u,
id                  └─┘                      └────────────────────────┘  └─────────────────────────┘
src      └──────┘  └─┘  └┘         └───┘ └─┘└────────────────────────┘ └─────────────────────────┘└┘
typ      └──────┘  └─┘ └┘      └───┘ └─┘└────────────────────────┘ └─────────────────────────┘└┘
doc      └──────┘  └─┘  └┘         └───┘ └─┘└────────────────────────┘ └─────────────────────────┘└┘
txt      └──────┘        └┘         └───┘ └─┘                                                      └┘
par      └──────┘        └┘         └───┘ └─┘                                                      └┘
pid      └───┘└─┘        └┘         └──┘ └─┘                                                      └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
702      have : ∀x∈s, fderiv_within 𝕜 (g ∘ f) s x = Φ (fderiv_within 𝕜 f s x),
id                                                 └───────────┘   
src      └─────┘ └┘                   └┘    └───────────┘    
typ      └─────┘ └┘                  └┘   └───────────┘ 
doc      └─────┘ └┘                    └┘     └───────────┘    
txt      └─────┘ └┘                    └┘                      
par      └─────┘ └┘                    └┘                      
pid      └───┘└┘ └┘                    └┘                      
st   ───────────────────────────────────────────────────────────────────────┘└─
703      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
704        rw [fderiv_within.comp x _ (hf.1 x hx) subset_preimage_univ (hs x hx),
id             └────────────────┘      └┘         └──────────────────┘  └┘  └┘
src        └──┘└────────────────┘ └─┘   └─┘   └┘└──────────────────┘      └──
typ        └──┘└────────────────┘ └─┘ └┘└─┘   └┘└──────────────────┘ └┘└┘└──
doc        └──┘                   └─┘   └─┘   └┘                          └──
txt        └──┘                   └─┘   └─┘   └┘                          └──
par        └──┘                   └─┘   └─┘   └┘                          └──
pid          └┘                   └─┘   └─┘   └┘                          └──
st   ──────────────────────────────────────────────────────────────────────────┘└─
705            fderiv_within_univ, hg.fderiv],
id             └────────────────┘
src  ─────────┘└────────────────┘└┘         
typ  ─────────┘└────────────────┘└┘└───────┘
doc  ─────────┘                  └┘         
txt  ─────────┘                  └┘         
par  ─────────┘                  └┘         
pid  ─────────┘                  └┘         
st   ───────────────────────────┘└─────────┘└──
706        rw differentiable_within_at_univ,
id            └───────────────────────────┘
src        └─┘└───────────────────────────┘
typ        └─┘└───────────────────────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────────────────────────────────┘└─
707        exact hg.differentiable_at },
id               └──────────────────┘
src        └────┘└──────────────────┘
typ        └────┘└──────────────────┘
doc        └────┘                    
txt        └────┘                    
par        └────┘                    
pid                                 
st   ────────────────────────────────┘└┘
708      apply times_cont_diff_on.congr_mono _ hs this (subset.refl _),
id             └───────────────────────────┘   └┘ └──┘  └─────────┘
src      └────┘└───────────────────────────┘└─┘       └─────────┘└─┘
typ      └────┘└───────────────────────────┘└─┘└┘└──┘ └─────────┘└─┘
doc      └────┘                             └─┘                  └─┘
txt      └────┘                             └─┘                  └─┘
par      └────┘                             └─┘                  └─┘
pid                                        └─┘                  └─┘
st   ────────────────────────────────────────────────────────────────┘└─
709      simp only [times_cont_diff_on_succ] at hf,
id                  └─────────────────────┘
src      └─────────┘└─────────────────────┘└─────┘
typ      └─────────┘└─────────────────────┘└─────┘
doc      └─────────┘                       └─────┘
txt      └─────────┘                       └─────┘
par      └─────────┘                       └─────┘
pid          └──┘└┘                       └───┘
st   ────────────────────────────────────────────┘└─
710      exact IH hf.2 hg.to_continuous_linear_map.is_bounded_linear_map_comp_left },
id             └┘ └┘   └─────────────────────────────────────────────────────────┘
src      └────┘    └─┘└─────────────────────────────────────────────────────────┘
typ      └────┘└┘└┘└─┘└─────────────────────────────────────────────────────────┘
doc      └────┘    └─┘└─────────────────────────────────────────────────────────┘
txt      └────┘    └─┘                                                           
par      └────┘    └─┘                                                           
pid               └─┘                                                           
st   ─────────────────────────────────────────────────────────────────────────────┘└┘
711    { rw times_cont_diff_on_top at hf ⊢,
id          └────────────────────┘
src      └─┘└────────────────────┘└──────┘
typ      └─┘└────────────────────┘└──────┘
doc      └─┘                      └──────┘
txt      └─┘                      └──────┘
par      └─┘                      └──────┘
pid                              └──────┘
st   ────────────────────────────────────┘└─
712      assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
713      apply Itop n (hf n) hg }
id             └──┘    └┘   └┘
src      └────┘         └┘  
typ      └────┘└──┘  └┘└┘└┘
doc      └────┘         └┘  
txt      └────┘         └┘  
par      └────┘         └┘  
pid                    └┘  
st   ──────────────────────────┘└─
714  end
st   ──┘
715  
716  /--
717  Composition by bounded linear maps preserves `C^n` functions.
718  -/
719  lemma times_cont_diff.comp_is_bounded_linear {n : with_top ℕ} {f : E → F} {g : F → G}
id                                                     └──────┘                     
src                                                    └──────┘ 
typ                                                    └──────┘                     
720    (hf : times_cont_diff 𝕜 n f) (hg : is_bounded_linear_map 𝕜 g) :
id           └─────────────┘           └───────────────────┘  
src          └─────────────┘              └───────────────────┘
typ          └─────────────┘           └───────────────────┘  
doc          └─────────────┘              └───────────────────┘
721    times_cont_diff 𝕜 n (λx, g (f x)) :=
id     └─────────────┘          
src    └─────────────┘
typ    └─────────────┘          
doc    └─────────────┘
722  times_cont_diff_on_univ.1 $ times_cont_diff_on.comp_is_bounded_linear (times_cont_diff_on_univ.2 hf)
id   └─────────────────────┘    └───────────────────────────────────────┘  └─────────────────────┘  └┘
src  └─────────────────────┘    └───────────────────────────────────────┘  └─────────────────────┘
typ  └─────────────────────┘    └───────────────────────────────────────┘  └─────────────────────┘  └┘
doc                              └───────────────────────────────────────┘
723    hg is_open_univ.unique_diff_on
id     └┘ └──────────┘└─────────────┘
src       └──────────┘└─────────────┘
typ    └┘ └──────────┘└─────────────┘
724  
725  /--
726  The cartesian product of `C^n` functions on domains is `C^n`.
727  -/
728  lemma times_cont_diff_on.prod {n : with_top ℕ} {s : set E} {f : E → F} {g : E → G}
id                                      └──────┘        └─┘                     
src                                     └──────┘        └─┘
typ                                     └──────┘        └─┘                     
729    (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) (hs : unique_diff_on 𝕜 s) :
id           └────────────────┘            └────────────────┘            └────────────┘  
src          └────────────────┘                └────────────────┘                └────────────┘
typ          └────────────────┘            └────────────────┘            └────────────┘  
doc          └────────────────┘                └────────────────┘                └────────────┘
730    times_cont_diff_on 𝕜 n (λx:E, (f x, g x)) s :=
id     └────────────────┘                
src    └────────────────┘            
typ    └────────────────┘                
doc    └────────────────┘
731  begin
st   └─────
732    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
733    induction n using with_top.nat_induction with n IH Itop generalizing F G,
id               
src    └────────┘ └───────────────────────────────────────────────────────────┘
typ    └────────┘└───────────────────────────────────────────────────────────┘
doc    └────────┘ └───────────────────────────────────────────────────────────┘
txt    └────────┘ └───────────────────────────────────────────────────────────┘
par    └────────┘ └───────────────────────────────────────────────────────────┘
pid              └───────────────────────────┘└─────────────┘└───────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
734    { rw times_cont_diff_on_zero at hf hg ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└─────────┘
typ      └─┘└─────────────────────┘└─────────┘
doc      └─┘                       └─────────┘
txt      └─┘                       └─────────┘
par      └─┘                       └─────────┘
pid                               └─────────┘
st   ───┘└───────────────────────────────────┘└─
735      exact continuous_on.prod hf hg },
id             └────────────────┘ └┘ └┘
src      └────┘└────────────────┘    
typ      └────┘└────────────────┘└┘└┘
doc      └────┘                      
txt      └────┘                      
par      └────┘                      
pid                                 
st   ──────────────────────────────────┘└┘
736    { rw times_cont_diff_on_succ at hf hg ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└─────────┘
typ      └─┘└─────────────────────┘└─────────┘
doc      └─┘                       └─────────┘
txt      └─┘                       └─────────┘
par      └─┘                       └─────────┘
pid                               └─────────┘
st   ───┘└───────────────────────────────────┘└─
737      refine ⟨differentiable_on.prod hf.1 hg.1, _⟩,
id               └────────────────────┘ └┘   └┘
src      └─────┘ └────────────────────┘  └─┘  └────┘
typ      └─────┘ └────────────────────┘└┘└─┘└┘└────┘
doc      └─────┘                         └─┘  └────┘
txt      └─────┘                         └─┘  └────┘
par      └─────┘                         └─┘  └────┘
pid                                     └─┘  └────┘
st   ───────────────────────────────────────────────┘└─
738      let F₁ := λx : E, (fderiv_within 𝕜 f s x, fderiv_within 𝕜 g s x),
id                                              └───────────┘   
src      └────────┘ └──┘ └┘                 └┘└───────────┘    
typ      └────────┘ └──┘└┘                └┘└───────────┘ 
doc      └────────┘ └──┘ └┘                  └┘└───────────┘    
txt      └────────┘ └──┘ └┘                  └┘                 
par      └────────┘ └──┘ └┘                  └┘                 
pid      └────┘└─┘ └──┘ └┘                  └┘                 
st   ───────────────────────────────────────────────────────────────────┘└─
739      let Φ : ((E →L[𝕜] F) × (E →L[𝕜] G)) → (E →L[𝕜] (F × G)) := λp, continuous_linear_map.prod p.1 p.2,
id                   └─┘                                          └────────────────────────┘
src      └──────┘   └─┘  └┘        └─┘            └────┘ └─┘└────────────────────────┘ └─┘ └┘
typ      └──────┘   └─┘  └┘        └─┘        └────┘ └─┘└────────────────────────┘ └─┘ └┘
doc      └──────┘   └─┘  └┘         └─┘            └────┘ └─┘└────────────────────────┘ └─┘ └┘
txt      └──────┘         └┘         └─┘            └────┘ └─┘                           └─┘ └┘
par      └──────┘         └┘         └─┘            └────┘ └─┘                           └─┘ └┘
pid      └───┘└─┘         └┘         └─┘            └┘└──┘ └─┘                           └─┘ └┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
740      have : times_cont_diff_on 𝕜 n (Φ ∘ F₁) s :=
id              └────────────────┘      └┘  
src      └─────┘└────────────────┘      └┘ └───
typ      └─────┘└────────────────┘ └┘└┘└───
doc      └─────┘└────────────────┘       └┘ └───
txt      └─────┘                         └┘ └───
par      └─────┘                         └┘ └───
pid      └───┘└┘                         └┘ └───
st   ────────────────────────────────────────────────
741        times_cont_diff_on.comp_is_bounded_linear (IH hf.2 hg.2) is_bounded_linear_map_prod_iso hs,
id         └───────────────────────────────────────┘  └┘ └┘   └┘    └────────────────────────────┘ └┘
src  ─────┘└───────────────────────────────────────┘     └─┘  └──┘└────────────────────────────┘
typ  ─────┘└───────────────────────────────────────┘ └┘└┘└─┘└┘└──┘└────────────────────────────┘└┘
doc  ─────┘└───────────────────────────────────────┘     └─┘  └──┘                              
txt  ─────┘                                              └─┘  └──┘                              
par  ─────┘                                              └─┘  └──┘                              
pid  ─────┘                                              └─┘  └──┘                              
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
742      apply times_cont_diff_on.congr_mono this hs (λx hx, _) (subset.refl _),
id             └───────────────────────────┘ └──┘ └┘             └─────────┘
src      └────┘└───────────────────────────┘        └───────┘ └─────────┘└─┘
typ      └────┘└───────────────────────────┘└──┘└┘  └───────┘ └─────────┘└─┘
doc      └────┘                                     └───────┘            └─┘
txt      └────┘                                     └───────┘            └─┘
par      └────┘                                     └───────┘            └─┘
pid                                                └───────┘            └─┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
743      apply differentiable_at.fderiv_within_prod (hf.1 x hx) (hg.1 x hx) (hs x hx) },
id             └──────────────────────────────────┘  └┘          └┘          └┘  └┘
src      └────┘└──────────────────────────────────┘   └─┘   └┘   └─┘   └┘      └┘
typ      └────┘└──────────────────────────────────┘ └┘└─┘   └┘ └┘└─┘   └┘ └┘└┘└┘
doc      └────┘                                       └─┘   └┘   └─┘   └┘      └┘
txt      └────┘                                       └─┘   └┘   └─┘   └┘      └┘
par      └────┘                                       └─┘   └┘   └─┘   └┘      └┘
pid                                                  └─┘   └┘   └─┘   └┘      
st   ────────────────────────────────────────────────────────────────────────────────┘└┘
744    { rw times_cont_diff_on_top at hf hg ⊢,
id          └────────────────────┘
src      └─┘└────────────────────┘└─────────┘
typ      └─┘└────────────────────┘└─────────┘
doc      └─┘                      └─────────┘
txt      └─┘                      └─────────┘
par      └─┘                      └─────────┘
pid                              └─────────┘
st   ───────────────────────────────────────┘└─
745      assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
746      apply Itop n (hf n) (hg n) }
id             └──┘    └┘     └┘ 
src      └────┘         └┘    └┘
typ      └────┘└──┘  └┘ └┘ └┘└┘
doc      └────┘         └┘    └┘
txt      └────┘         └┘    └┘
par      └────┘         └┘    └┘
pid                    └┘    
st   ──────────────────────────────┘└─
747  end
st   ──┘
748  
749  /--
750  The cartesian product of `C^n` functions is `C^n`.
751  -/
752  lemma times_cont_diff.prod {n : with_top ℕ} {f : E → F} {g : E → G}
id                                   └──────┘                     
src                                  └──────┘ 
typ                                  └──────┘                     
753    (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) :
id           └─────────────┘           └─────────────┘   
src          └─────────────┘              └─────────────┘
typ          └─────────────┘           └─────────────┘   
doc          └─────────────┘              └─────────────┘
754    times_cont_diff 𝕜 n (λx:E, (f x, g x)) :=
id     └─────────────┘             
src    └─────────────┘            
typ    └─────────────┘             
doc    └─────────────┘
755  times_cont_diff_on_univ.1 $ times_cont_diff_on.prod (times_cont_diff_on_univ.2 hf)
id   └─────────────────────┘    └─────────────────────┘  └─────────────────────┘  └┘
src  └─────────────────────┘    └─────────────────────┘  └─────────────────────┘
typ  └─────────────────────┘    └─────────────────────┘  └─────────────────────┘  └┘
doc                              └─────────────────────┘
756    (times_cont_diff_on_univ.2 hg) is_open_univ.unique_diff_on
id      └─────────────────────┘  └┘  └──────────┘└─────────────┘
src     └─────────────────────┘      └──────────┘└─────────────┘
typ     └─────────────────────┘  └┘  └──────────┘└─────────────┘
757  
758  /--
759  The composition of `C^n` functions on domains is `C^n`.
760  -/
761  lemma times_cont_diff_on.comp {n : with_top ℕ} {s : set E} {t : set F} {g : F → G} {f : E → F}
id                                      └──────┘        └─┘        └─┘                     
src                                     └──────┘        └─┘         └─┘
typ                                     └──────┘        └─┘        └─┘                     
762    (hg : times_cont_diff_on 𝕜 n g t) (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s)
id           └────────────────┘            └────────────────┘            └────────────┘  
src          └────────────────┘                └────────────────┘                └────────────┘
typ          └────────────────┘            └────────────────┘            └────────────┘  
doc          └────────────────┘                └────────────────┘                └────────────┘
763    (st : s ⊆ f ⁻¹' t) : times_cont_diff_on 𝕜 n (g ∘ f) s :=
id              └─┘     └────────────────┘        
src               └─┘      └────────────────┘        
typ             └─┘     └────────────────┘        
doc                └─┘      └────────────────┘
764  begin
st   └─────
765    tactic.unfreeze_local_instances,
id     └─────────────────────────────┘
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
par    └─────────────────────────────┘
st   ───────────────────────────────────
766    induction n using with_top.nat_induction with n IH Itop generalizing E F G,
id               
src    └────────┘ └─────────────────────────────────────────────────────────────┘
typ    └────────┘└─────────────────────────────────────────────────────────────┘
doc    └────────┘ └─────────────────────────────────────────────────────────────┘
txt    └────────┘ └─────────────────────────────────────────────────────────────┘
par    └────────┘ └─────────────────────────────────────────────────────────────┘
pid              └───────────────────────────┘└─────────────┘└─────────────────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
767    { rw times_cont_diff_on_zero at hf hg ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└─────────┘
typ      └─┘└─────────────────────┘└─────────┘
doc      └─┘                       └─────────┘
txt      └─┘                       └─────────┘
par      └─┘                       └─────────┘
pid                               └─────────┘
st   ───┘└───────────────────────────────────┘└─
768      exact continuous_on.comp hg hf st },
id             └────────────────┘ └┘ └┘ └┘
src      └────┘└────────────────┘      
typ      └────┘└────────────────┘└┘└┘└┘
doc      └────┘                        
txt      └────┘                        
par      └────┘                        
pid                                   
st   ─────────────────────────────────────┘└┘
769    { rw times_cont_diff_on_succ at hf hg ⊢,
id          └─────────────────────┘
src      └─┘└─────────────────────┘└─────────┘
typ      └─┘└─────────────────────┘└─────────┘
doc      └─┘                       └─────────┘
txt      └─┘                       └─────────┘
par      └─┘                       └─────────┘
pid                               └─────────┘
st   ───┘└───────────────────────────────────┘└─
770      /- We have to show that the derivative of g ∘ f is C^n, given that g and f are C^(n+1).
st   ────────────────────────────────────────────────────────────────────────────────────────────
771      By the chain rule, this derivative is Dg(f x) ⬝ Df(x). This is the composition of
st   ──────────────────────────────────────────────────────────────────────────────────────
772      x ↦ (Dg (f x), Df (x)) with the product of bounded linear maps, which is bilinear and therefore
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
773      C^∞. By the induction assumption, it suffices to show that x ↦ (Dg (f x), Df (x)) is C^n. It
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
774      is even enough to show that each component is C^n. This follows from the assumptions on f and g,
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
775      and the inductive assumption.
st   ──────────────────────────────────
776      -/
st   ───────
777      refine ⟨differentiable_on.comp hg.1 hf.1 st, _⟩,
id               └────────────────────┘ └┘   └┘   └┘
src      └─────┘ └────────────────────┘  └─┘  └─┘  └──┘
typ      └─────┘ └────────────────────┘└┘└─┘└┘└─┘└┘└──┘
doc      └─────┘                         └─┘  └─┘  └──┘
txt      └─────┘                         └─┘  └─┘  └──┘
par      └─────┘                         └─┘  └─┘  └──┘
pid                                     └─┘  └─┘  └──┘
st   ──────────────────────────────────────────────────┘└─
778      have : ∀x∈s, fderiv_within 𝕜 (g ∘ f) s x =
id                                               
src      └─────┘ └┘                   └┘  
typ      └─────┘ └┘                   └┘  
doc      └─────┘ └┘                    └┘   
txt      └─────┘ └┘                    └┘   
par      └─────┘ └┘                    └┘   
pid      └───┘└┘ └┘                    └┘   
st   ───────────────────────────────────────────────
779        continuous_linear_map.comp (fderiv_within 𝕜 g t (f x)) (fderiv_within 𝕜 f s x),
id         └────────────────────────┘                            └───────────┘   
src  ─────┘└────────────────────────┘                    └─┘ └───────────┘    
typ  ─────┘└────────────────────────┘                  └─┘ └───────────┘ 
doc  ─────┘└────────────────────────┘                    └─┘ └───────────┘    
txt  ─────┘                                              └─┘                  
par  ─────┘                                              └─┘                  
pid  ─────┘                                              └─┘                  
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
780      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
781        apply fderiv_within.comp x _ (hf.1 x hx) st (hs x hx),
id               └────────────────┘      └┘         └┘  └┘  └┘
src        └────┘└────────────────┘ └─┘   └─┘   └┘        
typ        └────┘└────────────────┘ └─┘ └┘└─┘   └┘└┘ └┘└┘
doc        └────┘                   └─┘   └─┘   └┘        
txt        └────┘                   └─┘   └─┘   └┘        
par        └────┘                   └─┘   └─┘   └┘        
pid                                └─┘   └─┘   └┘        
st   ──────────────────────────────────────────────────────────┘└─
782        exact hg.1 _ (st hx) },
id               └┘      └┘ └┘
src        └────┘  └───┘     └┘
typ        └────┘└┘└───┘ └┘└┘└┘
doc        └────┘  └───┘     └┘
txt        └────┘  └───┘     └┘
par        └────┘  └───┘     └┘
pid               └───┘     
st   ──────────────────────────┘└┘
783      apply times_cont_diff_on.congr _ hs this,
id             └──────────────────────┘   └┘ └──┘
src      └────┘└──────────────────────┘└─┘  
typ      └────┘└──────────────────────┘└─┘└┘└──┘
doc      └────┘                        └─┘  
txt      └────┘                        └─┘  
par      └────┘                        └─┘  
pid                                   └─┘  
st   ───────────────────────────────────────────┘└─
784      have A : times_cont_diff_on 𝕜 n (λx, fderiv_within 𝕜 g t (f x)) s :=
id                └────────────────┘         └───────────┘          
src      └───────┘└────────────────┘    └─┘└───────────┘      └─┘ └───
typ      └───────┘└────────────────┘   └─┘└───────────┘  └─┘└───
doc      └───────┘└────────────────┘    └─┘└───────────┘      └─┘ └───
txt      └───────┘                      └─┘                   └─┘ └───
par      └───────┘                      └─┘                   └─┘ └───
pid      └────┘└─┘                      └─┘                   └─┘ └───
st   ─────────────────────────────────────────────────────────────────────────
785        IH hg.2 (times_cont_diff_on_succ.2 hf).of_succ hs st,
id         └┘ └┘    └─────────────────────┘   └┘          └┘ └┘
src  ─────┘    └─┘ └─────────────────────┘└─┘  └────────┘  
typ  ─────┘└┘└┘└─┘ └─────────────────────┘└─┘└┘└────────┘└┘└┘
doc  ─────┘    └─┘                        └─┘  └────────┘  
txt  ─────┘    └─┘                        └─┘  └────────┘  
par  ─────┘    └─┘                        └─┘  └────────┘  
pid  ─────┘    └─┘                        └─┘  └────────┘  
st   ─────────────────────────────────────────────────────────┘└─
786      have B : times_cont_diff_on 𝕜 n (λx, fderiv_within 𝕜 f s x) s := hf.2,
id                └────────────────┘         └───────────┘            └┘
src      └───────┘└────────────────┘    └─┘└───────────┘    └┘ └──┘  └┘
typ      └───────┘└────────────────┘   └─┘└───────────┘  └┘└──┘└┘└┘
doc      └───────┘└────────────────┘    └─┘└───────────┘    └┘ └──┘  └┘
txt      └───────┘                      └─┘                 └┘ └──┘  └┘
par      └───────┘                      └─┘                 └┘ └──┘  └┘
pid      └────┘└─┘                      └─┘                 └┘ └──┘  └┘
st   ────────────────────────────────────────────────────────────────────────┘└─
787      have C : times_cont_diff_on 𝕜 n (λx:E, (fderiv_within 𝕜 f s x, fderiv_within 𝕜 g t (f x))) s :=
id                └────────────────┘                                 └───────────┘           
src      └───────┘└────────────────┘    └┘ └┘                 └┘└───────────┘      └──┘ └───
typ      └───────┘└────────────────┘   └┘└┘                 └┘└───────────┘  └──┘└───
doc      └───────┘└────────────────┘    └┘ └┘                  └┘└───────────┘      └──┘ └───
txt      └───────┘                      └┘ └┘                  └┘                   └──┘ └───
par      └───────┘                      └┘ └┘                  └┘                   └──┘ └───
pid      └────┘└─┘                      └┘ └┘                  └┘                   └──┘ └───
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
788        times_cont_diff_on.prod B A hs,
id         └─────────────────────┘   └┘
src  ─────┘└─────────────────────┘  
typ  ─────┘└─────────────────────┘└┘
doc  ─────┘└─────────────────────┘  
txt  ─────┘                         
par  ─────┘                         
pid  ─────┘                         
st   ───────────────────────────────────┘└─
789      have D : times_cont_diff_on 𝕜 n (λ(p : (E →L[𝕜] F) × (F →L[𝕜] G)), p.2.comp p.1) univ :=
id                └────────────────┘             └─┘                               └──┘
src      └───────┘└────────────────┘    └───┘  └─┘  └┘        └──┘ └──────┘ └──┘└──┘└───
typ      └───────┘└────────────────┘   └───┘ └─┘  └┘     └──┘ └──────┘ └──┘└──┘└───
doc      └───────┘└────────────────┘    └───┘  └─┘  └┘         └──┘ └──────┘ └──┘    └───
txt      └───────┘                      └───┘        └┘         └──┘ └──────┘ └──┘    └───
par      └───────┘                      └───┘        └┘         └──┘ └──────┘ └──┘    └───
pid      └────┘└─┘                      └───┘        └┘         └──┘ └──────┘ └──┘    └───
st   ─────────────────────────────────────────────────────────────────────────────────────────────
790        is_bounded_bilinear_map_comp.times_cont_diff.times_cont_diff_on is_open_univ.unique_diff_on,
id         └─────────────────────────────────────────────────────────────┘ └─────────────────────────┘
src  ─────┘└─────────────────────────────────────────────────────────────┘└─────────────────────────┘
typ  ─────┘└─────────────────────────────────────────────────────────────┘└─────────────────────────┘
doc  ─────┘                                                               
txt  ─────┘                                                               
par  ─────┘                                                               
pid  ─────┘                                                               
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
791      exact IH D C hs (subset_univ _) },
id             └┘   └┘  └─────────┘
src      └────┘       └─────────┘└──┘
typ      └────┘└┘└┘ └─────────┘└──┘
doc      └────┘                  └──┘
txt      └────┘                  └──┘
par      └────┘                  └──┘
pid                             └─┘
st   ───────────────────────────────────┘└┘
792    { rw times_cont_diff_on_top at hf hg ⊢,
id          └────────────────────┘
src      └─┘└────────────────────┘└─────────┘
typ      └─┘└────────────────────┘└─────────┘
doc      └─┘                      └─────────┘
txt      └─┘                      └─────────┘
par      └─┘                      └─────────┘
pid                              └─────────┘
st   ───────────────────────────────────────┘└─
793      assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
794      apply Itop n (hg n) (hf n) hs st }
id             └──┘    └┘     └┘   └┘ └┘
src      └────┘         └┘    └┘    
typ      └────┘└──┘  └┘ └┘ └┘└┘└┘└┘
doc      └────┘         └┘    └┘    
txt      └────┘         └┘    └┘    
par      └────┘         └┘    └┘    
pid                    └┘    └┘    
st   ────────────────────────────────────┘└─
795  end
st   ──┘
796  
797  /--
798  The composition of a C^n function on domain with a C^n function is C^n.
799  -/
800  lemma times_cont_diff.comp_times_cont_diff_on {n : with_top ℕ} {s : set E} {g : F → G} {f : E → F}
id                                                      └──────┘        └─┘                     
src                                                     └──────┘        └─┘
typ                                                     └──────┘        └─┘                     
801    (hg : times_cont_diff 𝕜 n g) (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) :
id           └─────────────┘           └────────────────┘            └────────────┘  
src          └─────────────┘              └────────────────┘                └────────────┘
typ          └─────────────┘           └────────────────┘            └────────────┘  
doc          └─────────────┘              └────────────────┘                └────────────┘
802    times_cont_diff_on 𝕜 n (g ∘ f) s :=
id     └────────────────┘        
src    └────────────────┘        
typ    └────────────────┘        
doc    └────────────────┘
803  (times_cont_diff_on_univ.2 hg).comp hf hs subset_preimage_univ
id    └─────────────────────┘  └┘ └──┘  └┘ └┘ └──────────────────┘
src   └─────────────────────┘     └──┘        └──────────────────┘
typ   └─────────────────────┘  └┘ └──┘  └┘ └┘ └──────────────────┘
doc                                └──┘
804  
805  /--
806  The composition of `C^n` functions is `C^n`.
807  -/
808  lemma times_cont_diff.comp {n : with_top ℕ} {g : F → G} {f : E → F}
id                                   └──────┘                     
src                                  └──────┘ 
typ                                  └──────┘                     
809    (hg : times_cont_diff 𝕜 n g) (hf : times_cont_diff 𝕜 n f) :
id           └─────────────┘           └─────────────┘   
src          └─────────────┘              └─────────────┘
typ          └─────────────┘           └─────────────┘   
doc          └─────────────┘              └─────────────┘
810    times_cont_diff 𝕜 n (g ∘ f) :=
id     └─────────────┘      
src    └─────────────┘        
typ    └─────────────┘      
doc    └─────────────┘
811  times_cont_diff_on_univ.1 $ times_cont_diff_on.comp (times_cont_diff_on_univ.2 hg)
id   └─────────────────────┘    └─────────────────────┘  └─────────────────────┘  └┘
src  └─────────────────────┘    └─────────────────────┘  └─────────────────────┘
typ  └─────────────────────┘    └─────────────────────┘  └─────────────────────┘  └┘
doc                              └─────────────────────┘
812    (times_cont_diff_on_univ.2 hf) is_open_univ.unique_diff_on (subset_univ _)
id      └─────────────────────┘  └┘  └──────────┘└─────────────┘  └─────────┘
src     └─────────────────────┘      └──────────┘└─────────────┘  └─────────┘
typ     └─────────────────────┘  └┘  └──────────┘└─────────────┘  └─────────┘
813  
814  /--
815  The bundled derivative of a `C^{n+1}` function is `C^n`.
816  -/
817  lemma times_cont_diff_on_fderiv_within_apply {m n : with_top  ℕ} {s : set E}
id                                                       └──────┘         └─┘ 
src                                                      └──────┘         └─┘
typ                                                      └──────┘         └─┘ 
818    {f : E → F} (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 ≤ n) :
id                     └────────────────┘            └────────────┘                
src                      └────────────────┘                └────────────┘                  
typ                    └────────────────┘            └────────────┘                
doc                      └────────────────┘                └────────────┘
819    times_cont_diff_on 𝕜 m (λp : E × E, (fderiv_within 𝕜 f s p.1 : E →L[𝕜] F) p.2) (set.prod s (univ : set E)) :=
id     └────────────────┘              └───────────┘         └─┘       └──────┘   └──┘   └─┘ 
src    └────────────────┘                  └───────────┘              └─┘          └──────┘    └──┘   └─┘
typ    └────────────────┘              └───────────┘         └─┘       └──────┘   └──┘   └─┘ 
doc    └────────────────┘                   └───────────┘               └─┘           └──────┘
820  begin
st   └─────
821    have U : unique_diff_on 𝕜 (set.prod s (univ : set E)) :=
id              └────────────┘   └──────┘   └──┘   └─┘ 
src    └───────┘└────────────┘  └──────┘  └──┘└─┘└─┘ └─────
typ    └───────┘└────────────┘ └──────┘ └──┘└─┘└─┘└─────
doc    └───────┘└────────────┘  └──────┘      └─┘    └─────
txt    └───────┘                              └─┘    └─────
par    └───────┘                              └─┘    └─────
pid    └────┘└─┘                              └─┘    └┘└───
st   ───────────────────────────────────────────────────────────
822      hs.prod unique_diff_on_univ,
id       └─────┘ └─────────────────┘
src  ───┘└─────┘└─────────────────┘
typ  ───┘└─────┘└─────────────────┘
doc  ───┘└─────┘
txt  ───┘       
par  ───┘       
pid  ───┘       
st   ──────────────────────────────┘└─
823    have A : times_cont_diff 𝕜 m (λp : (E →L[𝕜] F) × E, p.1 p.2),
id              └─────────────┘             └─┘    
src    └───────┘└─────────────┘    └──┘  └─┘  └┘ └┘ └─┘ └─┘
typ    └───────┘└─────────────┘   └──┘  └─┘└┘└┘ └─┘ └─┘
doc    └───────┘└─────────────┘    └──┘  └─┘  └┘  └┘ └─┘ └─┘
txt    └───────┘                   └──┘        └┘  └┘ └─┘ └─┘
par    └───────┘                   └──┘        └┘  └┘ └─┘ └─┘
pid    └────┘└─┘                   └──┘        └┘  └┘ └─┘ └─┘
st   ─────────────────────────────────────────────────────────────┘└─
824    { apply is_bounded_bilinear_map.times_cont_diff,
id             └─────────────────────────────────────┘
src      └────┘└─────────────────────────────────────┘
typ      └────┘└─────────────────────────────────────┘
doc      └────┘└─────────────────────────────────────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└───────────────────────────────────────────┘└─
825      exact is_bounded_bilinear_map_apply },
id             └───────────────────────────┘
src      └────┘└───────────────────────────┘
typ      └────┘└───────────────────────────┘
doc      └────┘                             
txt      └────┘                             
par      └────┘                             
pid                                        
st   ───────────────────────────────────────┘└┘
826    have B : times_cont_diff_on 𝕜 m
id              └────────────────┘   
src    └───────┘└────────────────┘  
typ    └───────┘└────────────────┘ 
doc    └───────┘└────────────────┘  
txt    └───────┘                    
par    └───────┘                    
pid    └────┘└─┘                    
st   ──────────────────────────────────
827      (λ (p : E × E), ((fderiv_within 𝕜 f s p.fst), p.snd)) (set.prod s univ),
id                      └───────────┘      └──┘    └──┘    └──────┘  └──┘
src  ───┘  └────┘   └─┘ └───────────┘    └──┘└─┘ └──┘└─┘ └──────┘ └──┘
typ  ───┘  └────┘ └─┘ └───────────┘  └──┘└─┘ └──┘└─┘ └──────┘└──┘
doc  ───┘  └────┘   └─┘  └───────────┘        └─┘     └─┘ └──────┘     
txt  ───┘  └────┘   └─┘                       └─┘     └─┘              
par  ───┘  └────┘   └─┘                       └─┘     └─┘              
pid  ───┘  └────┘   └─┘                       └─┘     └─┘              
st   ──────────────────────────────────────────────────────────────────────────┘└─
828    { apply times_cont_diff_on.prod _ _ U,
id             └─────────────────────┘     
src      └────┘└─────────────────────┘└───┘
typ      └────┘└─────────────────────┘└───┘
doc      └────┘└─────────────────────┘└───┘
txt      └────┘                       └───┘
par      └────┘                       └───┘
pid                                  └───┘
st   ───┘└─────────────────────────────────┘└─
829      { have I : times_cont_diff_on 𝕜 m (λ (x : E), fderiv_within 𝕜 f s x) s :=
id                  └────────────────┘               └───────────┘        
src        └───────┘└────────────────┘    └────┘ └─┘└───────────┘    └┘ └───
typ        └───────┘└────────────────┘   └────┘└─┘└───────────┘  └┘└───
doc        └───────┘└────────────────┘    └────┘ └─┘└───────────┘    └┘ └───
txt        └───────┘                      └────┘ └─┘                 └┘ └───
par        └───────┘                      └────┘ └─┘                 └┘ └───
pid        └────┘└─┘                      └────┘ └─┘                 └┘ └───
st   ─────┘└───────────────────────────────────────────────────────────────────────
830          times_cont_diff_on_fderiv_within hf hmn,
id           └──────────────────────────────┘ └┘ └─┘
src  ───────┘└──────────────────────────────┘  
typ  ───────┘└──────────────────────────────┘└┘└─┘
doc  ───────┘                                  
txt  ───────┘                                  
par  ───────┘                                  
pid  ───────┘                                  
st   ──────────────────────────────────────────────┘└─
831        have J : times_cont_diff_on 𝕜 m (λ (x : E × E), x.1) (set.prod s univ) :=
id                  └────────────────┘                        └──────┘  └──┘
src        └───────┘└────────────────┘    └────┘   └─┘ └──┘ └──────┘ └──┘└────
typ        └───────┘└────────────────┘  └────┘  └─┘ └──┘ └──────┘└──┘└────
doc        └───────┘└────────────────┘    └────┘   └─┘ └──┘ └──────┘     └────
txt        └───────┘                      └────┘   └─┘ └──┘              └────
par        └───────┘                      └────┘   └─┘ └──┘              └────
pid        └────┘└─┘                      └────┘   └─┘ └──┘              └───
st   ────────────────────────────────────────────────────────────────────────────────
832          times_cont_diff_fst.times_cont_diff_on U,
id           └────────────────────────────────────┘ 
src  ───────┘└────────────────────────────────────┘
typ  ───────┘└────────────────────────────────────┘
doc  ───────┘└────────────────────────────────────┘
txt  ───────┘                                      
par  ───────┘                                      
pid  ───────┘                                      
st   ───────────────────────────────────────────────┘└─
833        exact times_cont_diff_on.comp I J U (prod_subset_preimage_fst _ _) },
id               └─────────────────────┘     └──────────────────────┘
src        └────┘└─────────────────────┘    └──────────────────────┘└────┘
typ        └────┘└─────────────────────┘ └──────────────────────┘└────┘
doc        └────┘└─────────────────────┘                            └────┘
txt        └────┘                                                   └────┘
par        └────┘                                                   └────┘
pid                                                                └───┘
st   ────────────────────────────────────────────────────────────────────────┘└┘
834      { apply times_cont_diff.times_cont_diff_on _ U,
id               └────────────────────────────────┘   
src        └────┘└────────────────────────────────┘└─┘
typ        └────┘└────────────────────────────────┘└─┘
doc        └────┘                                  └─┘
txt        └────┘                                  └─┘
par        └────┘                                  └─┘
pid                                               └─┘
st   ─────────────────────────────────────────────────┘└─
835        apply is_bounded_linear_map.times_cont_diff,
id               └───────────────────────────────────┘
src        └────┘└───────────────────────────────────┘
typ        └────┘└───────────────────────────────────┘
doc        └────┘└───────────────────────────────────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────────────────────────┘└─
836        apply is_bounded_linear_map.snd } },
id               └───────────────────────┘
src        └────┘└───────────────────────┘
typ        └────┘└───────────────────────┘
doc        └────┘                         
txt        └────┘                         
par        └────┘                         
pid                                      
st   ─────────────────────────────────────┘└──┘
837    exact A.comp_times_cont_diff_on B U
id           └───────────────────────┘  
src    └────┘└───────────────────────┘  
typ    └────┘└───────────────────────┘
doc    └────┘└───────────────────────┘  
txt    └────┘                           
par    └────┘                           
pid                                    
st   ─────────────────────────────────────┘
838  end
st   └─┘
839  
840  /--
841  The bundled derivative of a `C^{n+1}` function is `C^n`.
842  -/
843  lemma times_cont_diff.times_cont_diff_fderiv_apply {n m : with_top ℕ} {s : set E} {f : E → F}
id                                                             └──────┘        └─┘           
src                                                            └──────┘        └─┘
typ                                                            └──────┘        └─┘           
844    (hf : times_cont_diff 𝕜 n f) (hmn : m + 1 ≤ n) :
id           └─────────────┘                 
src          └─────────────┘                    
typ          └─────────────┘                 
doc          └─────────────┘
845    times_cont_diff 𝕜 m (λp : E × E, (fderiv 𝕜 f p.1 : E →L[𝕜] F) p.2) :=
id     └─────────────┘              └────┘        └─┘   
src    └─────────────┘                  └────┘            └─┘      
typ    └─────────────┘              └────┘        └─┘   
doc    └─────────────┘                   └────┘             └─┘ 
846  begin
st   └─────
847    rw ← times_cont_diff_on_univ at ⊢ hf,
id          └─────────────────────┘
src    └───┘└─────────────────────┘└──────┘
typ    └───┘└─────────────────────┘└──────┘
doc    └───┘                       └──────┘
txt    └───┘                       └──────┘
par    └───┘                       └──────┘
pid      └─┘                       └──────┘
st   ─────────────────────────────────────┘└─
848    rw [← fderiv_within_univ, ← univ_prod_univ],
id           └────────────────┘    └────────────┘
src    └────┘└────────────────┘└──┘└────────────┘
typ    └────┘└────────────────┘└──┘└────────────┘
doc    └────┘                  └──┘              
txt    └────┘                  └──┘              
par    └────┘                  └──┘              
pid      └──┘                  └──┘              
st   ─────────────────────────┘└────────────────┘└──
849    exact times_cont_diff_on_fderiv_within_apply hf unique_diff_on_univ hmn
id           └────────────────────────────────────┘ └┘ └─────────────────┘ └─┘
src    └────┘└────────────────────────────────────┘  └─────────────────┘   
typ    └────┘└────────────────────────────────────┘└┘└─────────────────┘└─┘
doc    └────┘└────────────────────────────────────┘                        
txt    └────┘                                                              
par    └────┘                                                              
pid                                                                       
st   ─────────────────────────────────────────────────────────────────────────┘
850  end
st   └─┘
851  
852  /--
853  The sum of two C^n functions on a domain is C^n.
854  -/
855  lemma times_cont_diff_on.add {n : with_top ℕ} {s : set E} {f g : E → F}
id                                     └──────┘        └─┘             
src                                    └──────┘        └─┘
typ                                    └──────┘        └─┘             
856    (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) (hs : unique_diff_on 𝕜 s) :
id           └────────────────┘            └────────────────┘            └────────────┘  
src          └────────────────┘                └────────────────┘                └────────────┘
typ          └────────────────┘            └────────────────┘            └────────────┘  
doc          └────────────────┘                └────────────────┘                └────────────┘
857    times_cont_diff_on 𝕜 n (λx, f x + g x) s :=
id     └────────────────┘             
src    └────────────────┘              
typ    └────────────────┘             
doc    └────────────────┘
858  begin
st   └─────
859    have : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
id            └─────────────┘                  
src    └─────┘└─────────────┘    └──┘  └┘ └─┘ └─┘
typ    └─────┘└─────────────┘  └──┘ └┘ └─┘ └─┘
doc    └─────┘└─────────────┘    └──┘   └┘ └─┘  └─┘
txt    └─────┘                   └──┘   └┘ └─┘  └─┘
par    └─────┘                   └──┘   └┘ └─┘  └─┘
pid    └───┘└┘                   └──┘   └┘ └─┘  └─┘
st   ───────────────────────────────────────────────────┘└─
860    { apply is_bounded_linear_map.times_cont_diff,
id             └───────────────────────────────────┘
src      └────┘└───────────────────────────────────┘
typ      └────┘└───────────────────────────────────┘
doc      └────┘└───────────────────────────────────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────────────────────────────────────────┘└─
861      exact is_bounded_linear_map.add is_bounded_linear_map.fst is_bounded_linear_map.snd },
id             └───────────────────────┘ └───────────────────────┘ └───────────────────────┘
src      └────┘└───────────────────────┘└───────────────────────┘└───────────────────────┘
typ      └────┘└───────────────────────┘└───────────────────────┘└───────────────────────┘
doc      └────┘                                                                           
txt      └────┘                                                                           
par      └────┘                                                                           
pid                                                                                      
st   ───────────────────────────────────────────────────────────────────────────────────────┘└┘
862    exact this.comp_times_cont_diff_on (hf.prod hg hs) hs
id           └──────────────────────────┘  └─────┘ └┘     └┘
src    └────┘└──────────────────────────┘ └─────┘    └┘  
typ    └────┘└──────────────────────────┘ └─────┘└┘  └┘└┘
doc    └────┘└──────────────────────────┘ └─────┘    └┘  
txt    └────┘                                        └┘  
par    └────┘                                        └┘  
pid                                                 └┘  
st   ───────────────────────────────────────────────────────┘
863  end
st   └─┘
864  
865  /--
866  The sum of two C^n functions is C^n.
867  -/
868  lemma times_cont_diff.add {n : with_top ℕ} {f g : E → F}
id                                  └──────┘             
src                                 └──────┘ 
typ                                 └──────┘             
869    (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) : times_cont_diff 𝕜 n (λx, f x + g x) :=
id           └─────────────┘           └─────────────┘       └─────────────┘           
src          └─────────────┘              └─────────────┘          └─────────────┘              
typ          └─────────────┘           └─────────────┘       └─────────────┘           
doc          └─────────────┘              └─────────────┘          └─────────────┘
870  begin
st   └─────
871    have : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
id            └─────────────┘                  
src    └─────┘└─────────────┘    └──┘  └┘ └─┘ └─┘
typ    └─────┘└─────────────┘  └──┘ └┘ └─┘ └─┘
doc    └─────┘└─────────────┘    └──┘   └┘ └─┘  └─┘
txt    └─────┘                   └──┘   └┘ └─┘  └─┘
par    └─────┘                   └──┘   └┘ └─┘  └─┘
pid    └───┘└┘                   └──┘   └┘ └─┘  └─┘
st   ───────────────────────────────────────────────────┘└─
872    { apply is_bounded_linear_map.times_cont_diff,
id             └───────────────────────────────────┘
src      └────┘└───────────────────────────────────┘
typ      └────┘└───────────────────────────────────┘
doc      └────┘└───────────────────────────────────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────────────────────────────────────────┘└─
873      exact is_bounded_linear_map.add is_bounded_linear_map.fst is_bounded_linear_map.snd },
id             └───────────────────────┘ └───────────────────────┘ └───────────────────────┘
src      └────┘└───────────────────────┘└───────────────────────┘└───────────────────────┘
typ      └────┘└───────────────────────┘└───────────────────────┘└───────────────────────┘
doc      └────┘                                                                           
txt      └────┘                                                                           
par      └────┘                                                                           
pid                                                                                      
st   ───────────────────────────────────────────────────────────────────────────────────────┘└┘
874    exact this.comp (hf.prod hg)
id           └───────┘  └─────┘ └┘
src    └────┘└───────┘ └─────┘  └┘
typ    └────┘└───────┘ └─────┘└┘└┘
doc    └────┘└───────┘ └─────┘  └┘
txt    └────┘                   └┘
par    └────┘                   └┘
pid                            
st   ──────────────────────────────┘
875  end
st   └─┘
876  
877  /--
878  The negative of a C^n function on a domain is C^n.
879  -/
880  lemma times_cont_diff_on.neg {n : with_top ℕ} {s : set E} {f : E → F}
id                                     └──────┘        └─┘           
src                                    └──────┘        └─┘
typ                                    └──────┘        └─┘           
881    (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) :
id           └────────────────┘            └────────────┘  
src          └────────────────┘                └────────────┘
typ          └────────────────┘            └────────────┘  
doc          └────────────────┘                └────────────┘
882    times_cont_diff_on 𝕜 n (λx, -f x) s :=
id     └────────────────┘          
src    └────────────────┘          
typ    └────────────────┘          
doc    └────────────────┘
883  begin
st   └─────
884    have : times_cont_diff 𝕜 n (λp : F, -p),
id            └─────────────┘           
src    └─────┘└─────────────┘    └──┘ └┘ 
typ    └─────┘└─────────────┘  └──┘└┘ 
doc    └─────┘└─────────────┘    └──┘ └┘  
txt    └─────┘                   └──┘ └┘  
par    └─────┘                   └──┘ └┘  
pid    └───┘└┘                   └──┘ └┘  
st   ────────────────────────────────────────┘└─
885    { apply is_bounded_linear_map.times_cont_diff,
id             └───────────────────────────────────┘
src      └────┘└───────────────────────────────────┘
typ      └────┘└───────────────────────────────────┘
doc      └────┘└───────────────────────────────────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────────────────────────────────────────┘└─
886      exact is_bounded_linear_map.neg is_bounded_linear_map.id },
id             └───────────────────────┘ └──────────────────────┘
src      └────┘└───────────────────────┘└──────────────────────┘
typ      └────┘└───────────────────────┘└──────────────────────┘
doc      └────┘                                                 
txt      └────┘                                                 
par      └────┘                                                 
pid                                                            
st   ────────────────────────────────────────────────────────────┘└┘
887    exact this.comp_times_cont_diff_on hf hs
id           └──────────────────────────┘ └┘ └┘
src    └────┘└──────────────────────────┘    
typ    └────┘└──────────────────────────┘└┘└┘
doc    └────┘└──────────────────────────┘    
txt    └────┘                                
par    └────┘                                
pid                                         
st   ──────────────────────────────────────────┘
888  end
st   └─┘
889  
890  /--
891  The negative of a C^n function is C^n.
892  -/
893  lemma times_cont_diff.neg {n : with_top ℕ} {f : E → F} (hf : times_cont_diff 𝕜 n f) :
id                                  └──────┘                   └─────────────┘   
src                                 └──────┘                     └─────────────┘
typ                                 └──────┘                   └─────────────┘   
doc                                                               └─────────────┘
894    times_cont_diff 𝕜 n (λx, -f x) :=
id     └─────────────┘        
src    └─────────────┘          
typ    └─────────────┘        
doc    └─────────────┘
895  begin
st   └─────
896    have : times_cont_diff 𝕜 n (λp : F, -p),
id            └─────────────┘           
src    └─────┘└─────────────┘    └──┘ └┘ 
typ    └─────┘└─────────────┘  └──┘└┘ 
doc    └─────┘└─────────────┘    └──┘ └┘  
txt    └─────┘                   └──┘ └┘  
par    └─────┘                   └──┘ └┘  
pid    └───┘└┘                   └──┘ └┘  
st   ────────────────────────────────────────┘└─
897    { apply is_bounded_linear_map.times_cont_diff,
id             └───────────────────────────────────┘
src      └────┘└───────────────────────────────────┘
typ      └────┘└───────────────────────────────────┘
doc      └────┘└───────────────────────────────────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────────────────────────────────────────┘└─
898      exact is_bounded_linear_map.neg is_bounded_linear_map.id },
id             └───────────────────────┘ └──────────────────────┘
src      └────┘└───────────────────────┘└──────────────────────┘
typ      └────┘└───────────────────────┘└──────────────────────┘
doc      └────┘                                                 
txt      └────┘                                                 
par      └────┘                                                 
pid                                                            
st   ────────────────────────────────────────────────────────────┘└┘
899    exact this.comp hf
id           └───────┘ └┘
src    └────┘└───────┘  
typ    └────┘└───────┘└┘
doc    └────┘└───────┘  
txt    └────┘           
par    └────┘           
pid                    
st   ────────────────────┘
900  end
st   └─┘
901  
902  /--
903  The difference of two C^n functions on a domain is C^n.
904  -/
905  lemma times_cont_diff_on.sub {n : with_top ℕ} {s : set E} {f g : E → F}
id                                     └──────┘        └─┘             
src                                    └──────┘        └─┘
typ                                    └──────┘        └─┘             
906    (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) (hs : unique_diff_on 𝕜 s) :
id           └────────────────┘            └────────────────┘            └────────────┘  
src          └────────────────┘                └────────────────┘                └────────────┘
typ          └────────────────┘            └────────────────┘            └────────────┘  
doc          └────────────────┘                └────────────────┘                └────────────┘
907    times_cont_diff_on 𝕜 n (λx, f x - g x) s :=
id     └────────────────┘             
src    └────────────────┘              
typ    └────────────────┘             
doc    └────────────────┘
908  hf.add (hg.neg hs) hs
id   └┘└──┘  └┘└──┘ └┘  └┘
src    └──┘    └──┘
typ  └┘└──┘  └┘└──┘ └┘  └┘
doc    └──┘    └──┘
909  
910  /--
911  The difference of two C^n functions is C^n.
912  -/
913  lemma times_cont_diff.sub {n : with_top ℕ} {f g : E → F}
id                                  └──────┘             
src                                 └──────┘ 
typ                                 └──────┘             
914    (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) :
id           └─────────────┘           └─────────────┘   
src          └─────────────┘              └─────────────┘
typ          └─────────────┘           └─────────────┘   
doc          └─────────────┘              └─────────────┘
915    times_cont_diff 𝕜 n (λx, f x - g x) :=
id     └─────────────┘           
src    └─────────────┘              
typ    └─────────────┘           
doc    └─────────────┘
916  hf.add hg.neg
id   └┘└──┘ └┘└──┘
src    └──┘   └──┘
typ  └┘└──┘ └┘└──┘
doc    └──┘   └──┘